diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index fd9b448e4..746ea11cd 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -743,6 +743,7 @@ void CHC::visitPublicGetter(FunctionCall const& _funCall)
 	{
 		auto const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
 		auto const& contractType = dynamic_cast<ContractType const&>(*access.expression().annotation().type);
+		state().writeStateVars(*m_currentContract, state().thisAddress());
 		state().readStateVars(contractType.contractDefinition(), expr(access.expression()));
 	}
 	SMTEncoder::visitPublicGetter(_funCall);
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol
new file mode 100644
index 000000000..56dc9c3fa
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_1.sol
@@ -0,0 +1,22 @@
+contract D {
+	uint public d;
+	function g() public {
+		++d;
+	}
+}
+
+contract C {
+	function f() public {
+		D a = new D();
+		assert(a.d() == 0); // should hold
+		a.g();
+		assert(a.d() == 1); // should hold
+		assert(a.d() == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (203-221): CHC: Assertion violation happens here.\nCounterexample:\n\na = 42\n\nTransaction trace:\nC.constructor()\nC.f()\n    D.g() -- trusted external call
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_2.sol
new file mode 100644
index 000000000..5da279fc9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_2.sol
@@ -0,0 +1,33 @@
+contract E {
+	uint public e;
+	function setE(uint _e) public {
+		e = _e;
+	}
+}
+
+contract D {
+	E e;
+	constructor(E _e) {
+		e = _e;
+	}
+	function setE(uint x) public {
+		e.setE(x);
+	}
+}
+
+contract C {
+	function f() public {
+		E e = new E();
+		D d = new D(e);
+		assert(e.e() == 0); // should hold
+		d.setE(42);
+		assert(e.e() == 42); // should hold
+		assert(e.e() == 2); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (344-362): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol
new file mode 100644
index 000000000..787f7f8a8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_1.sol
@@ -0,0 +1,17 @@
+contract C {
+	uint public x;
+
+	function f() public {
+		x = 2;
+		x = 3;
+		uint y = this.x();
+		assert(y == 3); // should hold
+		assert(y == 2); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (127-141): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol
new file mode 100644
index 000000000..054c76082
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/external_getter_this_2.sol
@@ -0,0 +1,18 @@
+contract C {
+	uint public x;
+
+	function f() public {
+		x = 2;
+		x = 3;
+		C c = this;
+		uint y = c.x();
+		assert(y == 3); // should hold
+		assert(y == 2); // should fail
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTExtCalls: trusted
+// SMTTargets: assert
+// ----
+// Warning 6328: (138-152): CHC: Assertion violation happens here.