diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 26cc35cb1..07c09646e 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -130,7 +130,7 @@ bool BMC::shouldInlineFunctionCall(
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	if (funType.kind() == FunctionType::Kind::External)
-		return isTrustedExternalCall(&_funCall.expression());
+		return isExternalCallToThis(&_funCall.expression());
 	else if (funType.kind() != FunctionType::Kind::Internal)
 		return false;
 
@@ -567,7 +567,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	if (shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract))
 		inlineFunctionCall(_funCall);
-	else if (isPublicGetter(_funCall.expression()))
+	else if (publicGetter(_funCall.expression()))
 	{
 		// Do nothing here.
 		// The processing happens in SMT Encoder, but we need to prevent the resetting of the state variables.
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index a99608ec6..fd9b448e4 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -736,6 +736,18 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	verificationTargetEncountered(&_funCall, VerificationTargetType::Assert, errorCondition);
 }
 
+void CHC::visitPublicGetter(FunctionCall const& _funCall)
+{
+	createExpr(_funCall);
+	if (encodeExternalCallsAsTrusted())
+	{
+		auto const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
+		auto const& contractType = dynamic_cast<ContractType const&>(*access.expression().annotation().type);
+		state().readStateVars(contractType.contractDefinition(), expr(access.expression()));
+	}
+	SMTEncoder::visitPublicGetter(_funCall);
+}
+
 void CHC::visitAddMulMod(FunctionCall const& _funCall)
 {
 	solAssert(_funCall.arguments().at(2), "");
@@ -887,7 +899,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 
 	if (
 		encodeExternalCallsAsTrusted() ||
-		isTrustedExternalCall(callExpr)
+		isExternalCallToThis(callExpr)
 	)
 	{
 		externalFunctionCallToTrustedCode(_funCall);
@@ -957,6 +969,9 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 
 void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 {
+	if (publicGetter(_funCall.expression()))
+		visitPublicGetter(_funCall);
+
 	solAssert(m_currentContract, "");
 
 	auto [callExpr, callOptions] = functionCallExpression(_funCall);
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index d36338665..d757b219b 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -110,6 +110,7 @@ private:
 	void popInlineFrame(CallableDeclaration const& _callable) override;
 
 	void visitAssert(FunctionCall const& _funCall);
+	void visitPublicGetter(FunctionCall const& _funCall) override;
 	void visitAddMulMod(FunctionCall const& _funCall) override;
 	void visitDeployment(FunctionCall const& _funCall);
 	void internalFunctionCall(FunctionCall const& _funCall);
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index e2e9f4ffb..9c7537cd0 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -646,7 +646,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		visitGasLeft(_funCall);
 		break;
 	case FunctionType::Kind::External:
-		if (isPublicGetter(_funCall.expression()))
+		if (publicGetter(_funCall.expression()))
 			visitPublicGetter(_funCall);
 		break;
 	case FunctionType::Kind::ABIDecode:
@@ -995,9 +995,8 @@ vector<string> structGetterReturnedMembers(StructType const& _structType)
 
 void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
 {
-	MemberAccess const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
-	auto var = dynamic_cast<VariableDeclaration const*>(access.annotation().referencedDeclaration);
-	solAssert(var, "");
+	auto var = publicGetter(_funCall.expression());
+	solAssert(var && var->isStateVariable(), "");
 	solAssert(m_context.knownExpression(_funCall), "");
 	auto paramExpectedTypes = replaceUserTypes(FunctionType(*var).parameterTypes());
 	auto actualArguments = _funCall.arguments();
@@ -2800,16 +2799,13 @@ smtutil::Expression SMTEncoder::contractAddressValue(FunctionCall const& _f)
 	solAssert(false, "Unreachable!");
 }
 
-bool SMTEncoder::isPublicGetter(Expression const& _expr) {
-	if (!isTrustedExternalCall(&_expr))
-		return false;
-	auto varDecl = dynamic_cast<VariableDeclaration const*>(
-		dynamic_cast<MemberAccess const&>(_expr).annotation().referencedDeclaration
-	);
-	return varDecl != nullptr;
+VariableDeclaration const* SMTEncoder::publicGetter(Expression const& _expr) const {
+	if (auto memberAccess = dynamic_cast<MemberAccess const*>(&_expr))
+		return dynamic_cast<VariableDeclaration const*>(memberAccess->annotation().referencedDeclaration);
+	return nullptr;
 }
 
-bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
+bool SMTEncoder::isExternalCallToThis(Expression const* _expr) {
 	auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
 	if (!memberAccess)
 		return false;
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index de70e7612..e81af6d4d 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -219,7 +219,7 @@ protected:
 	void visitTypeConversion(FunctionCall const& _funCall);
 	void visitStructConstructorCall(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);
-	void visitPublicGetter(FunctionCall const& _funCall);
+	virtual void visitPublicGetter(FunctionCall const& _funCall);
 
 	/// @returns true if @param _contract is set for analysis in the settings
 	/// and it is not abstract.
@@ -227,7 +227,10 @@ protected:
 	/// @returns true if @param _source is set for analysis in the settings.
 	bool shouldAnalyze(SourceUnit const& _source) const;
 
-	bool isPublicGetter(Expression const& _expr);
+	/// @returns the state variable returned by a public getter if
+	/// @a _expr is a call to a public getter,
+	/// otherwise nullptr.
+	VariableDeclaration const* publicGetter(Expression const& _expr) const;
 
 	smtutil::Expression contractAddressValue(FunctionCall const& _f);
 
@@ -394,9 +397,9 @@ protected:
 	/// otherwise nullptr.
 	MemberAccess const* isEmptyPush(Expression const& _expr) const;
 
-	/// @returns true if the given identifier is a contract which is known and trusted.
+	/// @returns true if the given expression is `this`.
 	/// This means we don't have to abstract away effects of external function calls to this contract.
-	static bool isTrustedExternalCall(Expression const* _expr);
+	static bool isExternalCallToThis(Expression const* _expr);
 
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.