Update test expectation

test/libsolidity/smtCheckerTests/array_members/pop_2d_unsafe.sol

@@ -8,3 +8,5 @@ contract C {
 		a[1].pop();
 	}
 }
+// ----
+// Warning: (111-121): Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol

@@ -6,3 +6,5 @@ contract C {
 		a.pop();
 	}
 }
+// ----
+// Warning: (83-90): Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol

@@ -10,3 +10,5 @@ contract C {
 		a.pop();
 	}
 }
+// ----
+// Warning: (150-157): Empty array "pop" detected here.

test/libsolidity/smtCheckerTests/array_members/push_2d_arg_1_unsafe.sol

@@ -9,3 +9,6 @@ contract C {
 		assert(a[0][a[0].length - 1] == y);
 	}
 }
+// ----
+// Warning: (162-177): Underflow (resulting value less than 0) happens here
+// Warning: (150-184): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_safe_aliasing.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f() public {
+		a.push();
+		uint[] storage b = a[0];
+		b.push(8);
+		assert(b[b.length - 1] == 8);
+		// Safe but fails due to aliasing.
+		assert(a[0][a[0].length - 1] == 8);
+	}
+}
+// ----
+// Warning: (217-232): Underflow (resulting value less than 0) happens here
+// Warning: (205-239): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint[][] a;
+	function f() public {
+		a.push();
+		a[0].push();
+		a[0][0] = 16;
+		uint[] storage b = a[0];
+		b[0] = 32;
+		assert(a[0][0] == 16);
+	}
+}
+// ----
+// Warning: (167-188): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_zero_2d_unsafe.sol

@@ -8,3 +8,5 @@ contract C {
 		assert(a[a.length - 1][0] == 100);
 	}
 }
+// ----
+// Warning: (111-144): Assertion violation happens here

test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol

@@ -7,3 +7,5 @@ contract C {
 		assert(a[a.length - 1] == 100);
 	}
 }
+// ----
+// Warning: (94-124): Assertion violation happens here