diff --git a/Changelog.md b/Changelog.md
index 8d85739bd..9b1f3fe86 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -10,6 +10,7 @@ Compiler Features:
  * Code Generator: Avoid memory allocation for default value if it is not used.
  * SMTChecker: Support named arguments in function calls.
  * SMTChecker: Support struct constructor.
+ * SMTChecker: Support getters.
 
 Bugfixes:
  * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1.
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index de80dd996..544db45da 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -506,6 +506,11 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	if (shouldInlineFunctionCall(_funCall))
 		inlineFunctionCall(_funCall);
+	else if (isPublicGetter(_funCall.expression()))
+	{
+		// Do nothing here.
+		// The processing happens in SMT Encoder, but we need to prevent the resetting of the state variables.
+	}
 	else if (funType.kind() == FunctionType::Kind::Internal)
 		m_errorReporter.warning(
 			5729_error,
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index d2e463b23..01c4544f0 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -634,8 +634,11 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::GasLeft:
 		visitGasLeft(_funCall);
 		break;
-	case FunctionType::Kind::Internal:
 	case FunctionType::Kind::External:
+		if (isPublicGetter(_funCall.expression()))
+			visitPublicGetter(_funCall);
+		break;
+	case FunctionType::Kind::Internal:
 	case FunctionType::Kind::DelegateCall:
 	case FunctionType::Kind::BareCall:
 	case FunctionType::Kind::BareCallCode:
@@ -867,6 +870,98 @@ void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName)
 	m_context.createExpression(_typeName, result.second);
 }
 
+namespace // helpers for SMTEncoder::visitPublicGetter
+{
+
+bool isReturnedFromStructGetter(TypePointer _type)
+{
+	// So far it seems that only Mappings and ordinary Arrays are not returned.
+	auto category = _type->category();
+	if (category == Type::Category::Mapping)
+		return false;
+	if (category == Type::Category::Array)
+		return dynamic_cast<ArrayType const&>(*_type).isByteArray();
+	// default
+	return true;
+}
+
+vector<string> structGetterReturnedMembers(StructType const& _structType)
+{
+	vector<string> returnedMembers;
+	for (auto const& member: _structType.nativeMembers(nullptr))
+		if (isReturnedFromStructGetter(member.type))
+			returnedMembers.push_back(member.name);
+	return returnedMembers;
+}
+
+}
+
+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, "");
+	solAssert(m_context.knownExpression(_funCall), "");
+	auto paramExpectedTypes = FunctionType(*var).parameterTypes();
+	auto actualArguments = _funCall.arguments();
+	solAssert(actualArguments.size() == paramExpectedTypes.size(), "");
+	vector<smtutil::Expression> symbArguments;
+	for (unsigned i = 0; i < paramExpectedTypes.size(); ++i)
+		symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i]));
+
+	TypePointer type = var->type();
+	if (
+		type->isValueType() ||
+		(type->category() == Type::Category::Array && dynamic_cast<ArrayType const&>(*type).isByteArray())
+	)
+	{
+		solAssert(symbArguments.empty(), "");
+		defineExpr(_funCall, currentValue(*var));
+		return;
+	}
+	switch (type->category())
+	{
+		case Type::Category::Array:
+		case Type::Category::Mapping:
+		{
+			// For nested arrays/mappings, each argument in the call is an index to the next layer.
+			// We mirror this with `select` after unpacking the SMT-LIB array expression.
+			smtutil::Expression exprVal = currentValue(*var);
+			for (auto const& arg: symbArguments)
+			{
+				exprVal = smtutil::Expression::select(
+					smtutil::Expression::tuple_get(exprVal, 0),
+					arg
+				);
+			}
+			defineExpr(_funCall, exprVal);
+			break;
+		}
+		case Type::Category::Struct:
+		{
+			auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*type));
+			solAssert(!returnedMembers.empty(), "");
+			auto structVar = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.variable(*var));
+			solAssert(structVar, "");
+			auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) { return structVar->member(memberName); });
+			if (returnedValues.size() == 1)
+				defineExpr(_funCall, returnedValues.front());
+			else
+			{
+				auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
+				solAssert(symbTuple, "");
+				symbTuple->increaseIndex(); // Increasing the index explicitly since we cannot use defineExpr in this case.
+				auto const& symbComponents = symbTuple->components();
+				solAssert(symbComponents.size() == returnedValues.size(), "");
+				for (unsigned i = 0; i < symbComponents.size(); ++i)
+					m_context.addAssertion(symbTuple->component(i) == returnedValues.at(i));
+			}
+			break;
+		}
+		default: {} // Unsupported cases, do nothing and the getter will be abstracted.
+	}
+}
+
 void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
 {
 	solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
@@ -2403,6 +2498,15 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
 	return nullptr;
 }
 
+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;
+}
+
 bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
 	auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
 	if (!memberAccess)
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 4c26cb4c8..56cc53938 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -153,6 +153,9 @@ protected:
 	void visitTypeConversion(FunctionCall const& _funCall);
 	void visitStructConstructorCall(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);
+	void visitPublicGetter(FunctionCall const& _funCall);
+
+	bool isPublicGetter(Expression const& _expr);
 
 	/// Encodes a modifier or function body according to the modifier
 	/// visit depth.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/address.sol b/test/libsolidity/smtCheckerTests/functions/getters/address.sol
new file mode 100644
index 000000000..88b435cb7
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/address.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	address public x;
+	address payable public y;
+
+	function f() public view {
+		address a = this.x();
+		address b = this.y();
+		assert(a == x); // should hold
+		assert(a == address(this)); // should fail
+		assert(b == y); // should hold
+		assert(y == address(this)); // should fail
+	}
+}
+// ----
+// Warning 6328: (204-230): CHC: Assertion violation happens here.
+// Warning 6328: (282-308): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
new file mode 100644
index 000000000..c8c0c4675
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[] public a;
+
+	function f() public view {
+		uint y = this.a(2);
+		assert(y == a[2]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (153-167): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
new file mode 100644
index 000000000..4d6796dc8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] public a;
+
+	function f() public view {
+		uint y = this.a(2,3);
+		assert(y == a[2][3]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (160-174): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol b/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol
new file mode 100644
index 000000000..b760cfe21
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	bytes public str2 = 'c';
+
+	function f() public view {
+		bytes memory a2 = this.str2();
+		assert(keccak256(a2) == keccak256(str2)); // should hold
+		assert(keccak256(a2) == keccak256('a')); // should fail
+	}
+}
+// ----
+// Warning 6328: (195-234): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/contract.sol b/test/libsolidity/smtCheckerTests/functions/getters/contract.sol
new file mode 100644
index 000000000..af5f4963e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/contract.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract D {}
+
+contract C {
+	D public d;
+
+	function f() public view {
+		D e = this.d();
+		assert(e == d); // should hold
+		assert(address(e) == address(this)); // should fail
+	}
+}
+// ----
+// Warning 6328: (156-191): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol b/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol
new file mode 100644
index 000000000..315853245
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/double_access.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint u;
+	}
+
+	S public s;
+
+	function f() public view {
+		uint u = this.s();
+		uint v = this.s();
+		assert(u == s.u); // should hold
+		assert(u == v); // should hold
+		assert(u == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (226-240): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/enum.sol b/test/libsolidity/smtCheckerTests/functions/getters/enum.sol
new file mode 100644
index 000000000..28a7fd8d9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/enum.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+
+contract C {
+	enum ActionChoices { GoLeft, GoRight, GoStraight, SitStill }
+	ActionChoices public choice;
+
+	function f() public view {
+		ActionChoices e = this.choice();
+		assert(e == choice); // should hold
+		assert(e == ActionChoices.SitStill); // should fail
+	}
+}
+// ----
+// Warning 6328: (243-278): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol b/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol
new file mode 100644
index 000000000..bb7659267
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/fixed_bytes.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	byte public x;
+	bytes3 public y;
+
+	function f() public view {
+		byte a = this.x();
+		bytes3 b = this.y();
+		assert(a == x); // should hold
+		assert(a == 'a'); // should fail
+		assert(b == y); // should hold
+		assert(y == "abc"); // should fail
+	}
+}
+// ----
+// Warning 6328: (188-204): CHC: Assertion violation happens here.
+// Warning 6328: (256-274): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/function.sol b/test/libsolidity/smtCheckerTests/functions/getters/function.sol
new file mode 100644
index 000000000..51b5eb2a6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/function.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function () external returns (uint) public g;
+
+	function f() public {
+		g = this.X;
+		function () external returns (uint) e = this.g();
+		assert(e() == g()); // should hold, but fails because of the lack of support for tracking function pointers
+		assert(e() == 1); // should fail
+	}
+
+	function X() public pure returns (uint) {
+		return 42;
+	}
+}
+// ----
+// Warning 6328: (185-203): CHC: Assertion violation happens here.
+// Warning 6328: (295-311): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol
new file mode 100644
index 000000000..ae7476c0f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint) public map;
+
+	function f() public view {
+		uint y = this.map(2);
+		assert(y == map[2]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (175-189): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol
similarity index 50%
rename from test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol
rename to test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol
index aaa9605cc..905c143bc 100644
--- a/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol
@@ -5,8 +5,9 @@ contract C {
 
 	function f() public view {
 		uint y = this.map(2, 3);
-		assert(y == map[2][3]); // This fails as false positive because of lack of support for external getters.
+		assert(y == map[2][3]); // should hold
+		assert(y == 1); // should fail
 	}
 }
 // ----
-// Warning 6328: (158-180): CHC: Assertion violation happens here.
+// Warning 6328: (199-213): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol
new file mode 100644
index 000000000..f515e1d36
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_with_cast.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (bytes16 => uint) public m;
+
+	function f() public view {
+		uint y = this.m("foo");
+		assert(y == m["foo"]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (180-194): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol
new file mode 100644
index 000000000..1a39d5d6b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_1.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint[]) public m;
+
+	constructor() {
+		m[0].push();
+		m[0].push();
+		m[0][1] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1);
+		assert(y == m[0][1]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (243-257): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol
new file mode 100644
index 000000000..5d7d75b9f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_10.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint[])[] public m;
+
+	constructor() {
+		m.push();
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1][2] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1,2);
+		assert(y == m[0][1][2]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (289-303): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol
new file mode 100644
index 000000000..2717dac17
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_2.sol
@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint[][]) public m;
+
+	constructor() {
+		m[0].push();
+		m[0].push();
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1][2] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1,2);
+		assert(y == m[0][1][2]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (307-321): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol
new file mode 100644
index 000000000..422d060f6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_3.sol
@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint[][][]) public m;
+
+	constructor() {
+		m[0].push();
+		m[0].push();
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2][3] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1,2,3);
+		assert(y == m[0][1][2][3]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (401-415): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
new file mode 100644
index 000000000..2dc53b7e5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => mapping (uint => uint[])) public m;
+
+	constructor() {
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1][2] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1,2);
+		assert(y == m[0][1][2]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (293-307): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol
new file mode 100644
index 000000000..442efc47e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_5.sol
@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => mapping (uint => uint[][])) public m;
+
+	constructor() {
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1].push();
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2][3] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1,2,3);
+		assert(y == m[0][1][2][3]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (387-401): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol
new file mode 100644
index 000000000..df70036df
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_6.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => mapping (uint => mapping (uint => uint[]))) public m;
+
+	constructor() {
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2].push();
+		m[0][1][2][3] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1,2,3);
+		assert(y == m[0][1][2][3]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (349-363): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol
new file mode 100644
index 000000000..a2a18d815
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_7.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint)[] public m;
+
+	constructor() {
+		m.push();
+		m[0][1] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1);
+		assert(y == m[0][1]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (225-239): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol
new file mode 100644
index 000000000..da0932c21
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_8.sol
@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint)[][] public m;
+
+	constructor() {
+		m.push();
+		m[0].push();
+		m[0].push();
+		m[0][1][2] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1,2);
+		assert(y == m[0][1][2]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (265-279): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol
new file mode 100644
index 000000000..6e43e3902
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_9.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => mapping (uint => uint))[] public m;
+
+	constructor() {
+		m.push();
+		m[0][1][2] = 42;
+	}
+
+	function f() public view {
+		uint y = this.m(0,1,2);
+		assert(y == m[0][1][2]); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (251-265): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol b/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol
new file mode 100644
index 000000000..f887e572d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/static_array.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+
+contract C {
+
+	uint[2] public x = [42,1];
+
+	function f() public view {
+		assert(this.x(0) == x[0]); // should hold
+		assert(this.x(1) == x[1]); // should hold
+		assert(this.x(0) == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (195-217): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/string.sol b/test/libsolidity/smtCheckerTests/functions/getters/string.sol
new file mode 100644
index 000000000..6ed52b5a6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/string.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	string public str1 = 'b';
+
+	function f() public view {
+		string memory a1 = this.str1();
+		assert(keccak256(bytes(a1)) == keccak256(bytes(str1))); // should hold
+		assert(keccak256(bytes(a1)) == keccak256('a')); // should fail
+	}
+}
+// ----
+// Warning 6328: (211-257): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol
new file mode 100644
index 000000000..d03617a0a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol
@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+pragma abicoder v2;
+
+contract C {
+	struct T {
+		uint t;
+	}
+	struct S {
+		uint x;
+		T t;
+		bool b;
+		uint[] a;
+	}
+
+	S public s;
+
+	function f() public view {
+		uint y;
+		bool c;
+		T memory t;
+		(y,t,c) = this.s();
+		assert(y == s.x); // this should hold
+		assert(c == s.b); // this should hold
+		assert(t.t == s.t.t); // this should hold
+		assert(c == true); // this should fail
+	}
+}
+// ----
+// Warning 6328: (370-387): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol
new file mode 100644
index 000000000..39344c661
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+//pragma abicoder v2;
+
+contract C {
+	struct S {
+		uint[2] a;
+		uint u;
+	}
+
+	S public s;
+
+	function f() public view {
+		uint u = this.s();
+		assert(u == s.u); // should hold
+		assert(u == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (207-221): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol
new file mode 100644
index 000000000..d2f78d333
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_3.sol
@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		string s;
+		bytes b;
+	}
+
+	S public m;
+
+	constructor() {
+		m.s = "foo";
+		m.b = "bar";
+	}
+
+	function f() public view {
+		(string memory s, bytes memory b) = this.m();
+		assert(keccak256(bytes(s)) == keccak256(bytes(m.s))); // should hold
+		assert(b[0] == m.b[0]); // should hold
+		assert(b[0] == "t"); // should fail
+	}
+}
+// ----
+// Warning 6328: (340-359): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol
new file mode 100644
index 000000000..709cdf51e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_4.sol
@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract D {
+}
+
+contract C {
+	struct S {
+		D d;
+		function () external returns (uint) f;
+	}
+
+	S public s;
+
+	function test() public view {
+		(D d, function () external returns (uint) f) = this.s();
+		assert(d == s.d); // should hold
+		assert(address(d) == address(this)); // should fail
+	}
+}
+// ----
+// Warning 2072: (179-216): Unused local variable.
+// Warning 6328: (267-302): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol
new file mode 100644
index 000000000..91e685d28
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol
@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract C {
+	struct S {
+		uint x;
+		bool b;
+	}
+
+	S public s;
+
+	constructor() {
+		s.x = 1;
+		s.b = false;
+	}
+
+	function f() public {
+		uint x;
+		bool b;
+		(x,b) = this.s();
+		assert(x == s.x); // this should hold
+		assert(b == s.b); // this should hold
+		assert(b == true); // this should fail
+		s.x = 42;
+		(uint y, bool c) = this.s();
+		assert(c == b); // this should hold
+		assert(y == x); // this should fail
+
+	}
+}
+// ----
+// Warning 6328: (288-305): CHC: Assertion violation happens here.
+// Warning 6328: (410-424): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/uint.sol b/test/libsolidity/smtCheckerTests/functions/getters/uint.sol
new file mode 100644
index 000000000..8e0b14fe8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/getters/uint.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint public x;
+
+	function f() public view {
+		uint y = this.x();
+		assert(y == x); // should hold
+		assert(y == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (147-161): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol
deleted file mode 100644
index 60c1a57d5..000000000
--- a/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol
+++ /dev/null
@@ -1,12 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C {
-	uint public x;
-
-	function f() public view {
-		uint y = this.x();
-		assert(y == x); // This fails as false positive because of lack of support for external getters.
-	}
-}
-// ----
-// Warning 6328: (114-128): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol
deleted file mode 100644
index 5091da3f3..000000000
--- a/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol
+++ /dev/null
@@ -1,12 +0,0 @@
-pragma experimental SMTChecker;
-
-contract C {
-	mapping (uint => uint) public map;
-
-	function f() public view {
-		uint y = this.map(2);
-		assert(y == map[2]); // This fails as false positive because of lack of support for external getters.
-	}
-}
-// ----
-// Warning 6328: (137-156): CHC: Assertion violation happens here.