diff --git a/test/libsolidity/smtCheckerTests/operators/slices_3.sol b/test/libsolidity/smtCheckerTests/operators/slices_3.sol
index fa901ea01..d23c08140 100644
--- a/test/libsolidity/smtCheckerTests/operators/slices_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/slices_3.sol
@@ -5,7 +5,8 @@ function f(int[] calldata b, uint256 start, uint256 end) public returns (int) {
     uint len = end - start;
     assert(len == s.length);
     for (uint i = 0; i < len; i++) {
-        assert(b[start:end][i] == s[i]);
+        // Removed because of Spacer nondeterminism.
+        //assert(b[start:end][i] == s[i]);
     }
     return s[0];
 }
@@ -13,5 +14,3 @@ function f(int[] calldata b, uint256 start, uint256 end) public returns (int) {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (226-257): CHC: Assertion violation might happen here.
-// Warning 4661: (226-257): BMC: Assertion violation happens here.