Erase pointer knowledge properly inside loops

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	function testUnboundedForLoop(uint n, uint[] memory b, uint[] memory c) public pure {
+		b[0] = 900;
+		uint[] memory a = b;
+		require(n > 0 && n < 100);
+		for (uint i = 0; i < n; i += 1) {
+			b[i] = i + 1;
+			c[i] = b[i];
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (281-301): Assertion violation happens here
+// Warning: (305-324): Assertion violation happens here
+// Warning: (328-347): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] a;
+
+	function testUnboundedForLoop(uint n, uint[] memory b, uint[] memory c) public {
+		b[0] = 900;
+		a = b;
+		require(n > 0 && n < 100);
+		for (uint i = 0; i < n; i += 1) {
+			b[i] = i + 1;
+			c[i] = b[i];
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (274-294): Assertion violation happens here
+// Warning: (321-340): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] b;
+	uint[] c;
+
+	function testUnboundedForLoop(uint n) public {
+		b[0] = 900;
+		uint[] memory a = b;
+		require(n > 0 && n < 100);
+		for (uint i = 0; i < n; i += 1) {
+			b[i] = i + 1;
+			c[i] = b[i];
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (265-285): Assertion violation happens here
+// Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] b;
+	uint[] c;
+
+	function testUnboundedForLoop(uint n) public {
+		b[0] = 900;
+		uint[] storage a = b;
+		require(n > 0 && n < 100);
+		for (uint i = 0; i < n; i += 1) {
+			b[i] = i + 1;
+			c[i] = b[i];
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (266-286): Assertion violation happens here
+// Warning: (290-309): Assertion violation happens here
+// Warning: (313-332): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	function testUnboundedForLoop(uint n, uint[] memory b, uint[] memory c) public pure {
+		b[0] = 900;
+		uint[] memory a = b;
+		require(n > 0 && n < 100);
+		uint i;
+		while (i < n) {
+			b[i] = i + 1;
+			c[i] = b[i];
+			++i;
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (281-301): Assertion violation happens here
+// Warning: (305-324): Assertion violation happens here
+// Warning: (328-347): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] a;
+
+	function testUnboundedForLoop(uint n, uint[] memory b, uint[] memory c) public {
+		b[0] = 900;
+		a = b;
+		require(n > 0 && n < 100);
+		uint i;
+		while (i < n) {
+			b[i] = i + 1;
+			c[i] = b[i];
+			++i;
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (274-294): Assertion violation happens here
+// Warning: (321-340): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] b;
+	uint[] c;
+
+	function testUnboundedForLoop(uint n) public {
+		b[0] = 900;
+		uint[] memory a = b;
+		require(n > 0 && n < 100);
+		uint i;
+		while (i < n) {
+			b[i] = i + 1;
+			c[i] = b[i];
+			++i;
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (265-285): Assertion violation happens here
+// Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] b;
+	uint[] c;
+
+	function testUnboundedForLoop(uint n) public {
+		b[0] = 900;
+		uint[] storage a = b;
+		require(n > 0 && n < 100);
+		uint i;
+		while (i < n) {
+			b[i] = i + 1;
+			c[i] = b[i];
+			++i;
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (266-286): Assertion violation happens here
+// Warning: (290-309): Assertion violation happens here
+// Warning: (313-332): Assertion violation happens here