diff --git a/Changelog.md b/Changelog.md
index 02da20254..18c427922 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -10,7 +10,7 @@ Compiler Features:
  * Commandline Interface: Prevent some incompatible commandline options from being used together.
  * NatSpec: Support NatSpec comments on events.
  * Yul Optimizer: Store knowledge about storage / memory after ``a := sload(x)`` / ``a := mload(x)``.
- * SMTChecker: Support to external calls to unknown code and to known view/pure functions.
+ * SMTChecker: Support external calls to unknown code.
 
 
 Bugfixes:
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 7c6bbdaee..20a945f12 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -592,6 +592,9 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	if (!function)
 		return;
 
+	for (auto var: function->returnParameters())
+		m_context.variable(*var)->increaseIndex();
+
 	auto preCallState = currentStateVariables();
 	bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
 		function->stateMutability() == StateMutability::Pure ||
@@ -602,7 +605,6 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 
 	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
 	m_context.addAssertion(nondet);
-	m_context.addAssertion(predicate(_funCall));
 
 	m_context.addAssertion(m_error.currentValue() == 0);
 }
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol
index cd08791e0..8aef1f312 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol
@@ -27,3 +27,5 @@ contract C {
 		assert(sig_1 == sig_2);
 	}
 }
+// ----
+// Warning 4661: (438-460): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol
index f650ce824..02813f1d7 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol
@@ -16,3 +16,4 @@ contract D
 	}
 }
 // ----
+// Warning 4661: (191-206): Assertion violation happens here