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.