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 3e5d910db..f6f1f3210 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,7 +14,7 @@ contract LoopFor2 {
 		uint i;
 		while (i < n) {
 			b[i] = i + 1;
-			c[i] = b[i];
+			//c[i] = b[i]; // Removed because of Spacer's nondeterminism
 			++i;
 		}
 		//assert(b[0] == c[0]); // Removed because of Spacer's nondeterminism
@@ -26,8 +26,6 @@ contract LoopFor2 {
 // SMTEngine: all
 // ----
 // Warning 6368: (288-292): CHC: Out of bounds access might happen here.
-// Warning 6368: (312-316): CHC: Out of bounds access might happen here.
-// Warning 6368: (305-309): CHC: Out of bounds access might happen here.
-// Warning 6368: (411-415): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\na = []\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
-// Warning 6328: (404-423): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
-// Warning 6328: (427-446): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [1, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
+// Warning 6368: (459-463): CHC: Out of bounds access happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\na = []\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
+// Warning 6328: (452-471): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)
+// Warning 6328: (475-494): CHC: Assertion violation happens here.\nCounterexample:\nb = [1, 0], c = [0, 0]\nn = 1\ni = 1\n\nTransaction trace:\nLoopFor2.constructor()\nState: b = [], c = []\nLoopFor2.p()\nState: b = [0], c = [0]\nLoopFor2.p()\nState: b = [0, 0], c = [0, 0]\nLoopFor2.testUnboundedForLoop(1)