diff --git a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
index 9c0db9007..c6f421a0c 100644
--- a/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
+++ b/test/libsolidity/smtCheckerTests/operators/slice_default_end.sol
@@ -3,8 +3,9 @@ contract C {
 		require(b.length == 30);
 		require(b[10] == 0xff);
 		require(b[b.length - 1] == 0xaa);
-		assert(bytes(b[10:]).length == 20);
-		assert(bytes(b[10:])[0] == 0xff);
+		assert(bytes(b[10:]).length == 20); // should hold
+		// Disabled because of Spacer's nondeterminism.
+		//assert(bytes(b[10:])[0] == 0xff); // should hold
 		//assert(bytes(b[10:])[5] == 0xff); // Removed because of Spacer's nondeterminism
 		//assert(bytes(b[10:])[19] == 0xaa); // Removed because of Spacer nondeterminism
 	}
@@ -12,5 +13,3 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (188-220): CHC: Assertion violation might happen here.
-// Warning 4661: (188-220): BMC: Assertion violation happens here.