diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index cf02ca77e..bd0746550 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1144,8 +1144,12 @@ void SMTEncoder::visitFunctionIdentifier(Identifier const& _identifier)
 void SMTEncoder::visitStructConstructorCall(FunctionCall const& _funCall)
 {
 	solAssert(*_funCall.annotation().kind == FunctionCallKind::StructConstructorCall, "");
-	auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
-	structSymbolicVar.assignAllMembers(applyMap(_funCall.sortedArguments(), [this](auto const& arg) { return expr(*arg); }));
+	if (smt::isNonRecursiveStruct(*_funCall.annotation().type))
+	{
+		auto& structSymbolicVar = dynamic_cast<smt::SymbolicStructVariable&>(*m_context.expression(_funCall));
+		structSymbolicVar.assignAllMembers(applyMap(_funCall.sortedArguments(), [this](auto const& arg) { return expr(*arg); }));
+	}
+
 }
 
 void SMTEncoder::endVisit(Literal const& _literal)
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_recursive_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_recursive_1.sol
new file mode 100644
index 000000000..1265adbb9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_recursive_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract Test {
+	struct RecursiveStruct {
+		RecursiveStruct[] vals;
+	}
+	function func() public pure {
+		RecursiveStruct[1] memory val = [ RecursiveStruct(new RecursiveStruct[](42)) ];
+	}
+}
+// ----
+// Warning 2072: (136-165): Unused local variable.
+// Warning 8364: (170-212): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
+// Warning 8364: (170-212): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_recursive_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_recursive_2.sol
new file mode 100644
index 000000000..08194e68b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_recursive_2.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+contract Test {
+	struct RecursiveStruct {
+		uint x;
+		RecursiveStruct[] vals;
+	}
+	function func() public pure {
+		RecursiveStruct memory val = RecursiveStruct(1, new RecursiveStruct[](42));
+		assert(val.x == 1);
+	}
+}
+// ----
+// Warning 8115: (146-172): Assertion checker does not yet support the type of this variable.
+// Warning 8364: (175-220): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
+// Warning 7650: (231-236): Assertion checker does not yet support this expression.
+// Warning 8364: (231-234): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
+// Warning 6328: (224-242): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nfunc()
+// Warning 8115: (146-172): Assertion checker does not yet support the type of this variable.
+// Warning 8364: (175-220): Assertion checker does not yet implement type struct Test.RecursiveStruct memory
+// Warning 7650: (231-236): Assertion checker does not yet support this expression.
+// Warning 8364: (231-234): Assertion checker does not yet implement type struct Test.RecursiveStruct memory