diff --git a/Changelog.md b/Changelog.md
index faab15472..95fac0730 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -17,6 +17,7 @@ Compiler Features:
 Bugfixes:
  * AST: Do not output value of Yul literal if it is not a valid UTF-8 string.
  * SMTChecker: Fix internal error on struct constructor with fixed bytes member initialized with string literal.
+ * SMTChecker: Fix internal error on external calls from the constructor.
  * Source Locations: Properly set source location of scoped blocks.
  * Standard JSON: Properly allow the ``inliner`` setting under ``settings.optimizer.details``.
  * Type Checker: Fix internal compiler error related to having mapping types in constructor parameter for abstract contracts.
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index ba2d68a75..23967ecd2 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -773,10 +773,10 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0);
 	// To capture the possibility of a reentrant call, we record in the call graph that the  current function
 	// can call any of the external methods of the current contract.
-	solAssert(m_currentContract && m_currentFunction, "");
-	for (auto const* definedFunction: contractFunctions(*m_currentContract))
-		if (!definedFunction->isConstructor() && definedFunction->isPublic())
-			m_callGraph[m_currentFunction].insert(definedFunction);
+	if (m_currentFunction)
+		for (auto const* definedFunction: contractFunctions(*m_currentContract))
+			if (!definedFunction->isConstructor() && definedFunction->isPublic())
+				m_callGraph[m_currentFunction].insert(definedFunction);
 
 	m_context.addAssertion(errorFlag().currentValue() == 0);
 }
@@ -788,7 +788,6 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 	auto kind = funType.kind();
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
-	solAssert(m_currentContract, "");
 	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	if (!function)
 		return;
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol
new file mode 100644
index 000000000..3cdf5d156
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol
@@ -0,0 +1,19 @@
+contract State {
+	function f(uint _x) public pure returns (uint) {
+		assert(_x < 100);
+		return _x;
+	}
+}
+contract C {
+	State s;
+	uint z = s.f(2);
+
+	function f() public view {
+		assert(z == 2); // should fail since we don't trust s.f's code
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
+// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol
new file mode 100644
index 000000000..cfd56271b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol
@@ -0,0 +1,16 @@
+contract C {
+	uint z = this.g(2);
+
+	function g(uint _x) public pure returns (uint) {
+		assert(_x > 0);
+		return _x;
+	}
+
+	function f() public view {
+		assert(z == 2); // should fail since we don't trust s.f's code
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0)
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
new file mode 100644
index 000000000..eb5cd97dd
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
@@ -0,0 +1,23 @@
+contract State {
+	function f(uint _x) public pure returns (uint) {
+		assert(_x < 100);
+		return _x;
+	}
+}
+contract C {
+	State s;
+	uint z;
+
+	constructor() {
+		z = s.f(2);
+	}
+
+	function f() public view {
+		assert(z == 2); // should fail since we don't trust s.f's code
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
+// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()