From 20e23171dad2379772305bfbcbe9d9f82a6b74a8 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Thu, 15 Jul 2021 12:13:04 +0200
Subject: [PATCH 1/3] Update tests to z3 4.8.12

---
 .../smtCheckerTests/abi/abi_encode_string_literal.sol     | 4 +---
 .../abi/abi_encode_with_selector_vs_sig.sol               | 3 ++-
 .../array_members/push_storage_ref_unsafe_aliasing.sol    | 2 +-
 .../smtCheckerTests/crypto/crypto_functions_fail.sol      | 8 ++------
 .../external_calls/external_call_from_constructor_3.sol   | 2 +-
 .../file_level/constants_at_file_level_referencing.sol    | 2 +-
 .../smtCheckerTests/file_level/free_function_1.sol        | 2 +-
 .../smtCheckerTests/file_level/libraries_from_free.sol    | 2 +-
 test/libsolidity/smtCheckerTests/file_level/recursion.sol | 6 ++++--
 .../smtCheckerTests/functions/getters/bytes.sol           | 4 +---
 .../smtCheckerTests/functions/getters/string.sol          | 4 +---
 .../smtCheckerTests/loops/while_nested_break_fail.sol     | 2 +-
 .../abstract_function_nondet_pow_no_abstraction.sol       | 2 --
 .../natspec/safe_assert_false_positive_pure.sol           | 2 +-
 .../smtCheckerTests/overflow/simple_overflow.sol          | 2 +-
 .../smtCheckerTests/overflow/unsigned_mul_overflow.sol    | 2 +-
 .../smtCheckerTests/special/abi_decode_simple.sol         | 2 +-
 test/libsolidity/smtCheckerTests/special/blockhash.sol    | 2 +-
 test/libsolidity/smtCheckerTests/special/event.sol        | 2 +-
 test/libsolidity/smtCheckerTests/special/msg_data.sol     | 2 +-
 .../try_catch/try_multiple_catch_clauses_2.sol            | 2 +-
 .../smtCheckerTests/types/array_aliasing_storage_5.sol    | 1 +
 .../struct/struct_array_struct_array_storage_unsafe_1.sol | 6 +++---
 23 files changed, 29 insertions(+), 37 deletions(-)

diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
index 3b2006215..6eb3fff73 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_string_literal.sol
@@ -19,15 +19,13 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (208-238): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (208-238): CHC: Assertion violation might happen here.
+// Warning 6328: (208-238): CHC: Assertion violation happens here.
 // Warning 1218: (286-316): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (286-316): CHC: Assertion violation might happen here.
 // Warning 1218: (453-483): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (453-483): CHC: Assertion violation might happen here.
 // Warning 1218: (532-562): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (532-562): CHC: Assertion violation might happen here.
-// Warning 4661: (208-238): BMC: Assertion violation happens here.
 // Warning 4661: (286-316): BMC: Assertion violation happens here.
 // Warning 4661: (453-483): BMC: Assertion violation happens here.
 // Warning 4661: (532-562): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
index b97f28955..b5346b049 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_vs_sig.sol
@@ -9,4 +9,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (294-324): CHC: Assertion violation happens here.
+// Warning 6328: (294-324): CHC: Assertion violation might happen here.
+// Warning 7812: (294-324): BMC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
index d51a5f9e2..402ea67b4 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_aliasing.sol
@@ -14,5 +14,5 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6368: (188-192): CHC: Out of bounds access happens here.\nCounterexample:\na = []\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
-// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22, 22], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
+// Warning 6368: (188-195): CHC: Out of bounds access happens here.\nCounterexample:\na = [[], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [25, 25, 25, 25, 25, 25, 25, 25], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15], [15, 15, 15, 15, 15, 15, 15, 15]]\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
 // Warning 6328: (181-202): CHC: Assertion violation happens here.\nCounterexample:\n\nb = [32]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
index 76868fa2b..f7104caf5 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
@@ -27,10 +27,6 @@ contract C {
 // ----
 // Warning 2072: (556-566): Unused local variable.
 // Warning 2072: (598-608): Unused local variable.
-// Warning 1218: (135-151): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (135-151): CHC: Assertion violation might happen here.
+// Warning 6328: (135-151): CHC: Assertion violation happens here.
 // Warning 6328: (272-288): CHC: Assertion violation happens here.
-// Warning 1218: (415-431): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (415-431): CHC: Assertion violation might happen here.
-// Warning 4661: (135-151): BMC: Assertion violation happens here.
-// Warning 4661: (415-431): BMC: Assertion violation happens here.
+// Warning 6328: (415-431): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
index eb5cd97dd..9d27d6d3b 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
@@ -20,4 +20,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
-// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
+// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol b/test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol
index 4082885b9..2af325964 100644
--- a/test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/constants_at_file_level_referencing.sol
@@ -58,7 +58,7 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (s2.sol:518-539): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = []\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call
+// Warning 6328: (s2.sol:518-539): CHC: Assertion violation happens here.\nCounterexample:\n\nr2 = []\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call
 // Warning 6328: (s2.sol:704-725): CHC: Assertion violation happens here.\nCounterexample:\n\nr1 = [3, 1, 2]\nr2 = [3, 1, 2]\nr3 = []\nz = 0\n\nTransaction trace:\nC.constructor()\nC.p()\n    C.f() -- internal call\n    C.g() -- internal call
 // Warning 6328: (s2.sol:890-911): CHC: Assertion violation happens here.
 // Warning 6328: (s2.sol:980-994): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
index 1da78ef51..87d565327 100644
--- a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
@@ -12,4 +12,4 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 // SMTEngine: all
 // ----
 // Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    fun(_x, []) -- internal call
-// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
+// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol b/test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol
index 9f0104c21..728f9f69f 100644
--- a/test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol
@@ -23,6 +23,6 @@ contract C {
 // ----
 // Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
 // Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
-// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n    fu() -- internal call\n        L.inter() -- internal call
+// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n    fu() -- internal call\n        L.inter() -- internal call
 // Warning 6328: (363-377): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n    fu() -- internal call\n        L.inter() -- internal call
 // Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
diff --git a/test/libsolidity/smtCheckerTests/file_level/recursion.sol b/test/libsolidity/smtCheckerTests/file_level/recursion.sol
index ae3e25e08..a10087ba5 100644
--- a/test/libsolidity/smtCheckerTests/file_level/recursion.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/recursion.sol
@@ -26,14 +26,16 @@ contract C {
 // Warning 4281: (118-130): CHC: Division by zero might happen here.
 // Warning 4984: (134-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (176-189): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (430-450): CHC: Assertion violation happens here.
+// Warning 6328: (430-450): CHC: Assertion violation might happen here.
+// Warning 6328: (454-474): CHC: Assertion violation might happen here.
 // Warning 6328: (478-498): CHC: Assertion violation might happen here.
 // Warning 6328: (502-527): CHC: Assertion violation might happen here.
 // Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (454-474): BMC: Assertion violation happens here.
 // Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 8065: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4661: (478-498): BMC: Assertion violation happens here.
 // Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 4661: (502-527): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol b/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol
index 01dec8bc1..875cd5455 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/bytes.sol
@@ -10,6 +10,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (162-201): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (162-201): CHC: Assertion violation might happen here.
-// Warning 4661: (162-201): BMC: Assertion violation happens here.
+// Warning 6328: (162-201): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/string.sol b/test/libsolidity/smtCheckerTests/functions/getters/string.sol
index 2f2319a16..c856ad514 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/string.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/string.sol
@@ -10,6 +10,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (178-224): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (178-224): CHC: Assertion violation might happen here.
-// Warning 4661: (178-224): BMC: Assertion violation happens here.
+// Warning 6328: (178-224): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol
index ecd34cf3a..5a1bc9395 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol
@@ -30,4 +30,4 @@ contract C
 // SMTEngine: all
 // ----
 // Warning 6328: (296-311): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 10\nb = false\nc = true\n\nTransaction trace:\nC.constructor()\nC.f(0, 9, false, true)
-// Warning 6328: (347-362): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 20\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false)
+// Warning 6328: (347-362): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(9, 0, true, false)
diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
index f3a6581ca..7ce8b9c06 100644
--- a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
+++ b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
@@ -33,11 +33,9 @@ contract C {
 // ====
 // SMTEngine: chc
 // ----
-// Warning 4984: (176-179): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4281: (435-447): CHC: Division by zero might happen here.
 // Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4281: (495-507): CHC: Division by zero might happen here.
 // Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 3944: (579-591): CHC: Underflow (resulting value less than 0) might happen here.
 // Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
diff --git a/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
index 03dd24475..464d9834a 100644
--- a/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
+++ b/test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol
@@ -26,4 +26,4 @@ contract C {
 // ----
 // Warning 2018: (33-335): Function state mutability can be restricted to view
 // Warning 2018: (457-524): Function state mutability can be restricted to pure
-// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\nz = 1\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call
+// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 1\nz = 0\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(1)\n    C.f1(1) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
index d872cb669..e8cf49a83 100644
--- a/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/simple_overflow.sol
@@ -4,4 +4,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935\nb = 1\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639935, 1)
+// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\na = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol
index 0a6d85a7e..045fcbff8 100644
--- a/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol
@@ -6,4 +6,4 @@ contract C  {
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819968\ny = 2\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 2)
+// Warning 4984: (80-85): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 2\ny = 57896044618658097711785492504343953926634992332820282019728792003956564819968\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 57896044618658097711785492504343953926634992332820282019728792003956564819968)
diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
index 5a6beef49..17e3b30d8 100644
--- a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
+++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
@@ -15,6 +15,6 @@ contract C {
 // Warning 2072: (152-156): Unused local variable.
 // Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
 // Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)
-// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\na1 = 7719\nb1 = 5\nc1 = 6\na2 = 7719\nb2 = 5\nc2 = 6\n\nTransaction trace:\nC.constructor()\nC.f([13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
+// Warning 6328: (220-236): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 13, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9]\na1 = 7719\nb1 = 5\nc1 = 6\na2 = 7719\nb2 = 5\nc2 = 6\n\nTransaction trace:\nC.constructor()\nC.f([9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 13, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9])
 // Warning 8364: (123-124): Assertion checker does not yet implement type type(contract C)
 // Warning 8364: (193-194): Assertion checker does not yet implement type type(contract C)
diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol
index 7c8b23052..c33aed968 100644
--- a/test/libsolidity/smtCheckerTests/special/blockhash.sol
+++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol
@@ -11,4 +11,4 @@ contract C
 // SMTEngine: all
 // ----
 // Warning 6328: (52-76): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 8365 }
-// Warning 6328: (80-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 32285 }
+// Warning 6328: (80-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 5853 }
diff --git a/test/libsolidity/smtCheckerTests/special/event.sol b/test/libsolidity/smtCheckerTests/special/event.sol
index 2788eeecd..a0a6d566b 100644
--- a/test/libsolidity/smtCheckerTests/special/event.sol
+++ b/test/libsolidity/smtCheckerTests/special/event.sol
@@ -27,4 +27,4 @@ contract C {
 // ----
 // Warning 6321: (247-251): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
 // Warning 6321: (397-401): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
-// Warning 6328: (407-416): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n    C.h_data() -- internal call\n    C.h_data() -- internal call
+// Warning 6328: (407-416): CHC: Assertion violation happens here.\nCounterexample:\nx = false\n\nTransaction trace:\nC.constructor()\nState: x = true\nC.h()\n    C.h_data() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol
index 5bdc754c4..5c42613d3 100644
--- a/test/libsolidity/smtCheckerTests/special/msg_data.sol
+++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol
@@ -23,4 +23,4 @@ contract C
 // SMTEngine: all
 // ----
 // Warning 6328: (120-147): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 30612 }
-// Warning 6328: (467-494): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 30612 }
+// Warning 6328: (467-494): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 11797 }
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
index 609b31fcd..9180119a1 100644
--- a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
@@ -20,4 +20,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (306-320): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (306-320): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
index 9f111dfb4..15500167d 100644
--- a/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol
@@ -33,6 +33,7 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
+// Warning 6368: (186-196): CHC: Out of bounds access might happen here.
 // Warning 6368: (329-333): CHC: Out of bounds access happens here.
 // Warning 6368: (342-346): CHC: Out of bounds access happens here.
 // Warning 6368: (355-359): CHC: Out of bounds access happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
index d1686e8c0..3d6cf0df4 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
@@ -41,8 +41,8 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (148-165): CHC: Assertion violation happens here.
-// Warning 6328: (183-202): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
+// Warning 6328: (148-165): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 0, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
+// Warning 6328: (183-202): CHC: Assertion violation happens here.
 // Warning 6328: (266-286): CHC: Assertion violation happens here.
 // Warning 6328: (404-427): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: []}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
-// Warning 6328: (578-604): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: [0, 0, 0, 0, 0, 6]}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
+// Warning 6328: (578-604): CHC: Assertion violation happens here.

From 5decccaf3a8f8fb9c2551355dc6a23120c2fb0c7 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Fri, 16 Jul 2021 13:01:17 +0200
Subject: [PATCH 2/3] update docker hashes and versions

---
 .circleci/config.yml                  | 16 ++++++++--------
 .circleci/osx_install_dependencies.sh | 16 +++++++++-------
 scripts/build_emscripten.sh           |  4 ++--
 3 files changed, 19 insertions(+), 17 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 054a60a28..93e9f93bd 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -9,20 +9,20 @@ version: 2.1
 parameters:
   ubuntu-2004-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-6
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:da44d7f78e093f7f0415abf07f7c1fd1c2ed4fa65fefea428821a05186c42ec9"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-7
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:af5a0c6ea5e113e477f5387955a862f9aea5cc74d9ceeb2377fc64e64088d200"
   ubuntu-2004-clang-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-6
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:c78dd9c48d393b57afe053aeb2d0d358a9f31ac85039a181724c2f8408d0bcf8"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-7
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:cb504c6456d4a2dd80b354acfd7429836da5acce4e394500c02d5740617f9d01"
   ubuntu-1604-clang-ossfuzz-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-9
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:5078e1d74ab6f4329e9218c2d8c0ebe2d42817a3d4c3c62ce887100cbe9bc739"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-10
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:ea15a35f6188360b425593c83e946660ab4ea4dac9b9c3bb3629e6ed57276b1d"
   emscripten-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:emscripten-5
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d28afb9624c2352ea40f157d1a321ffac77f54a21e33a8e8744f9126b780ded4"
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-6
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:092da5817bc032c91a806b4f73db2a1a31e5cc4c066d94d43eedd9f365df7154"
 
 orbs:
   win: circleci/windows@2.2.0
diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh
index f1dd4f11b..55d406946 100755
--- a/.circleci/osx_install_dependencies.sh
+++ b/.circleci/osx_install_dependencies.sh
@@ -48,13 +48,15 @@ then
   ./scripts/install_obsolete_jsoncpp_1_7_4.sh
 
   # z3
-  wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-osx-10.15.7.zip
-  unzip z3-4.8.10-x64-osx-10.15.7.zip
-  rm -f z3-4.8.10-x64-osx-10.15.7.zip
-  cp z3-4.8.10-x64-osx-10.15.7/bin/libz3.a /usr/local/lib
-  cp z3-4.8.10-x64-osx-10.15.7/bin/z3 /usr/local/bin
-  cp z3-4.8.10-x64-osx-10.15.7/include/* /usr/local/include
-  rm -rf z3-4.8.10-x64-osx-10.15.7
+  z3_version="z3-4.8.12"
+  osx_version="osx-10.15.7"
+  wget "https://github.com/Z3Prover/z3/releases/download/$z3_version/$z3_version-x64-$osx_version.zip"
+  unzip "$z3_version-x64-$osx_version.zip"
+  rm -f "$z3_version-x64-$osx_version.zip"
+  cp "$z3_version-x64-$osx_version/bin/libz3.a" /usr/local/lib
+  cp "$z3_version-x64-$osx_version/bin/z3" /usr/local/bin
+  cp "$z3_version-x64-$osx_version"/include/* /usr/local/include
+  rm -rf "$z3_version-x64-$osx_version"
 
   # evmone
   wget https://github.com/ethereum/evmone/releases/download/v0.7.0/evmone-0.7.0-darwin-x86_64.tar.gz
diff --git a/scripts/build_emscripten.sh b/scripts/build_emscripten.sh
index 1e0e35924..667d63708 100755
--- a/scripts/build_emscripten.sh
+++ b/scripts/build_emscripten.sh
@@ -34,7 +34,7 @@ else
     BUILD_DIR="$1"
 fi
 
-# solbuildpackpusher/solidity-buildpack-deps:emscripten-4
+# solbuildpackpusher/solidity-buildpack-deps:emscripten-6
 docker run -v "$(pwd):/root/project" -w /root/project \
-    solbuildpackpusher/solidity-buildpack-deps@sha256:434719d8104cab47712dd1f56f255994d04eb65b802c0d382790071c1a0c074b \
+    solbuildpackpusher/solidity-buildpack-deps@sha256:092da5817bc032c91a806b4f73db2a1a31e5cc4c066d94d43eedd9f365df7154 \
     ./scripts/ci/build_emscripten.sh "$BUILD_DIR"

From e46abd0ca149b6639703f0c5f600ed00dbe581ce Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Fri, 16 Jul 2021 15:44:36 +0200
Subject: [PATCH 3/3] Update tests due to nondeterminism

---
 .../abi/abi_encode_packed_array_slice_2.sol   |  1 +
 .../crypto/crypto_functions_fail.sol          | 16 ++++++++++------
 .../file_level/free_function_1.sol            |  5 +++--
 .../smtCheckerTests/file_level/recursion.sol  | 19 +++----------------
 .../functions/constructor_state_value.sol     |  3 ++-
 .../inheritance/fallback_receive.sol          |  7 ++++---
 .../smtCheckerTests/inheritance/receive.sol   |  7 ++++---
 ...y_local_storage_access_inside_function.sol |  5 +++--
 ...act_function_nondet_pow_no_abstraction.sol |  9 +++------
 .../smtCheckerTests/special/blockhash.sol     |  5 +++--
 .../smtCheckerTests/special/msg_data.sol      |  5 +++--
 .../try_multiple_catch_clauses_2.sol          |  3 ++-
 .../types/string_literal_comparison_2.sol     |  5 +++--
 ...uct_array_struct_array_memory_unsafe_2.sol |  1 +
 ...ct_array_struct_array_storage_unsafe_1.sol |  5 +++--
 15 files changed, 48 insertions(+), 48 deletions(-)

diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol
index 7f8b98806..fc34ff1c7 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_array_slice_2.sol
@@ -28,6 +28,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 2072: (643-658): Unused local variable.
 // Warning 6328: (298-328): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
index f7104caf5..8485b89a6 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
@@ -7,12 +7,14 @@ contract C {
 	function s(bytes memory b0, bytes memory b1) public pure {
 		bytes32 s0 = sha256(b0);
 		bytes32 s1 = sha256(b1);
-		assert(s0 == s1);
+		// Disabled because of Spacer nondeterminism.
+		//assert(s0 == s1);
 	}
 	function r(bytes memory b0, bytes memory b1) public pure {
 		bytes32 r0 = ripemd160(b0);
 		bytes32 r1 = ripemd160(b1);
-		assert(r0 == r1);
+		// Disabled because of Spacer nondeterminism.
+		//assert(r0 == r1);
 	}
 	function e(bytes32 h0, uint8 v0, bytes32 r0, bytes32 s0, bytes32 h1, uint8 v1, bytes32 r1, bytes32 s1) public pure {
 		address a0 = ecrecover(h0, v0, r0, s0);
@@ -25,8 +27,10 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 2072: (556-566): Unused local variable.
-// Warning 2072: (598-608): Unused local variable.
+// Warning 2072: (218-228): Unused local variable.
+// Warning 2072: (245-255): Unused local variable.
+// Warning 2072: (405-415): Unused local variable.
+// Warning 2072: (435-445): Unused local variable.
+// Warning 2072: (656-666): Unused local variable.
+// Warning 2072: (698-708): Unused local variable.
 // Warning 6328: (135-151): CHC: Assertion violation happens here.
-// Warning 6328: (272-288): CHC: Assertion violation happens here.
-// Warning 6328: (415-431): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
index 87d565327..5dd951521 100644
--- a/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/free_function_1.sol
@@ -10,6 +10,7 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    fun(_x, []) -- internal call
-// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 5, 5, 5, 16, 5, 5, 20, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
+// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6368: (289-294): CHC: Out of bounds access happens here.
diff --git a/test/libsolidity/smtCheckerTests/file_level/recursion.sol b/test/libsolidity/smtCheckerTests/file_level/recursion.sol
index a10087ba5..f461861e9 100644
--- a/test/libsolidity/smtCheckerTests/file_level/recursion.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/recursion.sol
@@ -13,29 +13,16 @@ contract C {
 	}
 	function f() public pure {
 		// All of these should hold but the SMTChecker can't prove them.
+		// Disabled because of Spacer nondet
+		/*
 		assert(g(0, 0) == 1);
 		assert(g(0, 1) == 0);
 		assert(g(1, 0) == 1);
 		assert(g(2, 3) == 8);
 		assert(g(3, 10) == 59049);
+		*/
 	}
 }
 // ====
 // SMTEngine: all
 // ----
-// Warning 4281: (118-130): CHC: Division by zero might happen here.
-// Warning 4984: (134-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 4984: (176-189): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (430-450): CHC: Assertion violation might happen here.
-// Warning 6328: (454-474): CHC: Assertion violation might happen here.
-// Warning 6328: (478-498): CHC: Assertion violation might happen here.
-// Warning 6328: (502-527): CHC: Assertion violation might happen here.
-// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4661: (454-474): BMC: Assertion violation happens here.
-// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4661: (478-498): BMC: Assertion violation happens here.
-// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4661: (502-527): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
index 5add9bf68..48819f839 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
@@ -12,5 +12,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (112-126): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(11)
+// Warning 6328: (112-126): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol b/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol
index 81b3d9a48..203484265 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/fallback_receive.sol
@@ -20,7 +20,8 @@ contract B is A {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (81-95): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.fallback()
-// Warning 6328: (130-144): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
-// Warning 6328: (256-270): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive(){ value: 10450 }
+// Warning 6328: (81-95): CHC: Assertion violation happens here.
+// Warning 6328: (130-144): CHC: Assertion violation happens here.
+// Warning 6328: (256-270): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/receive.sol b/test/libsolidity/smtCheckerTests/inheritance/receive.sol
index a88ff75f8..f55b9efd6 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/receive.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/receive.sol
@@ -20,7 +20,8 @@ contract B is A {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive()
-// Warning 6328: (144-158): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
-// Warning 6328: (267-281): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.receive()
+// Warning 6328: (95-109): CHC: Assertion violation happens here.
+// Warning 6328: (144-158): CHC: Assertion violation happens here.
+// Warning 6328: (267-281): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol
index a95bb8731..797f6ae76 100644
--- a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol
+++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol
@@ -17,8 +17,9 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 7737: (83-149): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
-// Warning 6328: (152-167): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\ni = 32\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
-// Warning 6328: (186-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\ni = 32\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
+// Warning 6328: (152-167): CHC: Assertion violation happens here.
+// Warning 6328: (186-200): CHC: Assertion violation happens here.
 // Warning 7737: (83-149): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
index 7ce8b9c06..dc4fc9ef1 100644
--- a/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
+++ b/test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol
@@ -7,6 +7,8 @@ contract C {
 	}
 
 	function pow(uint base, uint exponent) internal pure returns (uint) {
+		// Disabled because of Spacer nondet
+		/*
 		if (base == 0) {
 			return 0;
 		}
@@ -28,14 +30,9 @@ contract C {
 			}
 		}
 		return base * y;
+		*/
 	}
 }
 // ====
 // SMTEngine: chc
 // ----
-// Warning 4281: (435-447): CHC: Division by zero might happen here.
-// Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 4281: (495-507): CHC: Division by zero might happen here.
-// Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol
index c33aed968..2a7cc39fa 100644
--- a/test/libsolidity/smtCheckerTests/special/blockhash.sol
+++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol
@@ -9,6 +9,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (52-76): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 8365 }
-// Warning 6328: (80-104): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(38){ value: 5853 }
+// Warning 6328: (52-76): CHC: Assertion violation happens here.
+// Warning 6328: (80-104): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/special/msg_data.sol b/test/libsolidity/smtCheckerTests/special/msg_data.sol
index 5c42613d3..90022508f 100644
--- a/test/libsolidity/smtCheckerTests/special/msg_data.sol
+++ b/test/libsolidity/smtCheckerTests/special/msg_data.sol
@@ -21,6 +21,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (120-147): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(){ value: 30612 }
-// Warning 6328: (467-494): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g(){ value: 11797 }
+// Warning 6328: (120-147): CHC: Assertion violation happens here.
+// Warning 6328: (467-494): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
index 9180119a1..d11d3a8a6 100644
--- a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
@@ -19,5 +19,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (306-320): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\nsuccess = false\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (306-320): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol
index 24a2652d8..81f513bd5 100644
--- a/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/string_literal_comparison_2.sol
@@ -9,6 +9,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (114-133): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 0\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)
-// Warning 6328: (137-157): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 52647538830022687173130149211684818290356179572910782152375644828738034597888\ny = 52647538830022687173130149211684818290356179572910782152375644828738034597888\nz = 52647538830022687173130149211684818290356179572910782152375644828738034597888\n\nTransaction trace:\nC.constructor()\nC.f(52647538830022687173130149211684818290356179572910782152375644828738034597888)
+// Warning 6328: (114-133): CHC: Assertion violation happens here.
+// Warning 6328: (137-157): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
index d34eb47ed..a1a40d64b 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_memory_unsafe_2.sol
@@ -36,5 +36,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (804-842): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
index 3d6cf0df4..662b4f1d2 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_array_struct_array_storage_unsafe_1.sol
@@ -40,9 +40,10 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (148-165): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 0, a: []}, a: [], ts: []}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
+// Warning 6328: (148-165): CHC: Assertion violation happens here.
 // Warning 6328: (183-202): CHC: Assertion violation happens here.
 // Warning 6328: (266-286): CHC: Assertion violation happens here.
-// Warning 6328: (404-427): CHC: Assertion violation happens here.\nCounterexample:\ns1 = {x: 2, t: {y: 3, a: []}, a: [0, 0, 4], ts: [{y: 0, a: []}, {y: 0, a: []}, {y: 0, a: []}, {y: 5, a: []}, {y: 0, a: []}, {y: 0, a: []}]}\n\nTransaction trace:\nC.constructor()\nState: s1 = {x: 0, t: {y: 0, a: []}, a: [], ts: []}\nC.f()
+// Warning 6328: (404-427): CHC: Assertion violation happens here.
 // Warning 6328: (578-604): CHC: Assertion violation happens here.