From 7b467a49d79a42c0091686de2f8ba5a26c9ac074 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= <kamil.sliwak@codepoets.it>
Date: Thu, 15 Apr 2021 16:28:06 +0200
Subject: [PATCH] Disable assertion that gives non-deterministic results in in
 slice tests for SMTChecker

---
 test/libsolidity/smtCheckerTests/operators/slices_3.sol | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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.