From 6aa6c5f5f946729eea5839dbf62551af04bd57a3 Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@usi.ch>
Date: Fri, 12 Mar 2021 19:33:45 +0100
Subject: [PATCH] [SMTChecker] Reset reference variables on assignment to a
 variable of reference type

---
 libsolidity/formal/SMTEncoder.cpp             |  4 ++++
 ...nment_contract_member_variable_array_3.sol | 21 +++++++++++++++++++
 .../smtCheckerTests/types/bytes_2.sol         |  2 ++
 3 files changed, 27 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 9e572b536..3398e308f 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2034,7 +2034,11 @@ void SMTEncoder::assignment(
 			m_context.newValue(*varDecl);
 	}
 	else if (auto varDecl = identifierToVariable(*left))
+	{
+		if (varDecl->hasReferenceOrMappingType())
+			resetReferences(*varDecl);
 		assignment(*varDecl, _right);
+	}
 	else if (
 		dynamic_cast<IndexAccess const*>(left) ||
 		dynamic_cast<MemberAccess const*>(left)
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol
new file mode 100644
index 000000000..0b69c3004
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable_array_3.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+contract A {
+	int[] a;
+	function f() public {
+		require(a.length == 1 && a[0] == 1);
+		int[] storage u = a;
+		assert(u[0] == 1); // should hold
+		int[] memory b = new int[](2);
+		a = b;
+		assert(u[0] == 1); // should fail
+		A.a = b;
+		assert(u[0] == 1); // should fail
+	}
+
+	function push_v(int x) public {
+		a.push(x);
+	}
+}
+// ----
+// Warning 6328: (220-237): CHC: Assertion violation happens here.
+// Warning 6328: (267-284): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/bytes_2.sol b/test/libsolidity/smtCheckerTests/types/bytes_2.sol
index dc41aa423..c53f4a7f3 100644
--- a/test/libsolidity/smtCheckerTests/types/bytes_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/bytes_2.sol
@@ -7,3 +7,5 @@ contract C
 		assert(b1[1] == b2[1]);
 	}
 }
+// ----
+// Warning 6328: (119-141): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(b1, b2)