diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol
index 1bd8c7517..7169b444e 100644
--- a/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol
+++ b/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol
@@ -7,10 +7,11 @@ contract Simple {
 		for (i = 0; i < n; ++i)
 			a[i] = i;
 		require(n > 1);
-		// Assertion is safe but current solver version cannot solve it.
+		// Assertion is safe but current solver version times out.
 		// Keep test for next solver release.
 		assert(a[n-1] > a[n-2]);
 	}
 }
 // ----
-// Warning: (267-290): Assertion violation happens here
+// Warning: (261-284): Error trying to invoke SMT solver.
+// Warning: (261-284): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol
deleted file mode 100644
index 6cb6cd6d9..000000000
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol
+++ /dev/null
@@ -1,23 +0,0 @@
-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: (312-331): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
index 7670ddb6d..92d1ded3e 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
@@ -14,11 +14,13 @@ contract LoopFor2 {
 			c[i] = b[i];
 			++i;
 		}
+		// Fails as false positive.
 		assert(b[0] == c[0]);
 		assert(a[0] == 900);
 		assert(b[0] == 900);
 	}
 }
 // ----
-// Warning: (290-309): Assertion violation happens here
-// Warning: (313-332): Assertion violation happens here
+// Warning: (296-316): Assertion violation happens here
+// Warning: (320-339): Assertion violation happens here
+// Warning: (343-362): Assertion violation happens here