diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 28026ec6f..11edafbae 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -853,17 +853,11 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 		""
 	);
 
-	bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall;
-
 	solAssert(m_currentContract, "");
 	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	if (function)
-	{
-		usesStaticCall |= function->stateMutability() == StateMutability::Pure ||
-			function->stateMutability() == StateMutability::View;
 		for (auto var: function->returnParameters())
 			m_context.variable(*var)->increaseIndex();
-	}
 
 	if (!m_currentFunction || m_currentFunction->isConstructor())
 		return;
@@ -883,7 +877,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 
 	auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
 
-	if (!usesStaticCall)
+	if (!usesStaticCall(_funCall))
 	{
 		state().newState();
 		for (auto const* var: m_stateVariables)
@@ -1164,6 +1158,14 @@ set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
 	return verificationTargetsIds;
 }
 
+bool CHC::usesStaticCall(FunctionCall const& _funCall)
+{
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
+	return (function && (function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall;
+}
+
 optional<CHC::CHCNatspecOption> CHC::natspecOptionFromString(string const& _option)
 {
 	static map<string, CHCNatspecOption> options{
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 9524d86dc..4aa2afe0d 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -136,6 +136,7 @@ private:
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
 	void setCurrentBlock(Predicate const& _block);
 	std::set<unsigned> transactionVerificationTargetsIds(ASTNode const* _txRoot);
+	bool usesStaticCall(FunctionCall const& _funCall);
 	//@}
 
 	/// SMT Natspec and abstraction helpers.