diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 2cc7f13fc..0bc6a1adc 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -215,9 +215,11 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		// This is done in endVisit(ContractDefinition).
 		if (_function.isConstructor())
 		{
-			auto constructorExit = createBlock(&_function, "exit_");
-			connectBlocks(m_currentBlock, predicate(*constructorExit));
-			setCurrentBlock(*constructorExit);
+			auto constructorExit = createSymbolicBlock(interfaceSort(), "constructor_exit_" + to_string(_function.id()));
+			connectBlocks(m_currentBlock, predicate(*constructorExit, currentStateVariables()));
+			clearIndices(m_currentContract, m_currentFunction);
+			auto stateExprs = currentStateVariables();
+			setCurrentBlock(*constructorExit, &stateExprs);
 		}
 		else
 		{
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol
new file mode 100644
index 000000000..eaa7c5dc4
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_hierarchy_mixed_chain_local_vars.sol
@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+contract F {
+	uint a;
+	constructor() public {
+		uint f = 2;
+		a = f;
+	}
+}
+
+contract E is F {}
+contract D is E {
+	constructor() public {
+		uint d = 3;
+		a = d;
+	}
+}
+contract C is D {}
+contract B is C {
+	constructor() public {
+		uint b = 4;
+		a = b;
+	}
+}
+
+contract A is B {
+	constructor(uint x) public {
+		uint a1 = 4;
+		uint a2 = 5;
+		assert(a == a1);
+		assert(a == a2);
+	}
+}
+// ----
+// Warning: (317-323): Unused function parameter. Remove or comment out the variable name to silence this warning.
+// Warning: (385-400): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_this.sol b/test/libsolidity/smtCheckerTests/functions/constructor_this.sol
new file mode 100644
index 000000000..0a308a166
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_this.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+    function f() public pure {}
+    constructor() public {
+        C c = this;
+        c.f(); // this does not warn now, but should warn in the future
+        this.f();
+        (this).f();
+    }
+}
+// ----
+// Warning: (204-208): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.
+// Warning: (223-227): "this" used in constructor. Note that external functions of a contract cannot be called while it is being constructed.