From 6fd76e830dded60101cdd503c5c4e70805367aaa Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 5 Mar 2021 15:50:39 +0100
Subject: [PATCH] Fix CHC cex order

---
 libsolidity/formal/CHC.cpp                    | 32 ++++++++++++++++---
 .../abi/abi_encode_array_slice_2.sol          | 20 ++++++------
 .../blockchain_state/transfer.sol             |  2 +-
 ...or_state_variable_init_chain_alternate.sol |  2 +-
 .../crypto/crypto_functions_fail.sol          | 10 +++---
 .../crypto/crypto_functions_not_same.sol      |  2 +-
 .../functions/constructor_state_value.sol     |  2 +-
 .../getters/nested_arrays_mappings_4.sol      |  4 ++-
 ...y_local_storage_access_inside_function.sol |  2 +-
 .../loops/while_2_break_fail.sol              |  2 +-
 .../overflow/signed_div_overflow.sol          |  2 +-
 .../special/abi_decode_simple.sol             |  2 +-
 .../smtCheckerTests/special/difficulty.sol    |  2 +-
 .../smtCheckerTests/special/event.sol         |  2 +-
 .../smtCheckerTests/special/this.sol          |  2 +-
 .../try_string_literal_to_fixed_bytes.sol     |  2 +-
 .../types/mapping_as_parameter_1.sol          |  2 +-
 .../types/mapping_equal_keys_2.sol            |  2 +-
 .../types/struct/struct_recursive_4.sol       |  8 +++--
 19 files changed, 64 insertions(+), 38 deletions(-)

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 1f6594d06..afca3e72b 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -38,6 +38,7 @@
 #include <z3_version.h>
 #endif
 
+#include <charconv>
 #include <queue>
 
 using namespace std;
@@ -949,8 +950,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 		if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
 		{
 			string suffix = contract->name() + "_" + to_string(contract->id());
-			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + suffix, PredicateType::Interface, contract);
-			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + suffix, PredicateType::NondetInterface, contract);
+			m_interfaces[contract] = createSymbolicBlock(interfaceSort(*contract, state()), "interface_" + uniquePrefix() + "_" + suffix, PredicateType::Interface, contract);
+			m_nondetInterfaces[contract] = createSymbolicBlock(nondetInterfaceSort(*contract, state()), "nondet_interface_" + uniquePrefix() + "_" + suffix, PredicateType::NondetInterface, contract);
 			m_constructorSummaries[contract] = createConstructorBlock(*contract, "summary_constructor");
 			m_contractInitializers[contract] = createConstructorBlock(*contract, "contract_initializer");
 
@@ -1104,7 +1105,7 @@ Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract
 {
 	return createSymbolicBlock(
 		constructorSort(_contract, state()),
-		_prefix + "_" + contractSuffix(_contract) + "_" + uniquePrefix(),
+		_prefix + "_" + uniquePrefix() + "_" + contractSuffix(_contract),
 		PredicateType::ConstructorSummary,
 		&_contract,
 		&_contract
@@ -1622,7 +1623,30 @@ map<unsigned, vector<unsigned>> CHC::summaryCalls(CHCSolverInterface::CexGraph c
 	map<unsigned, vector<unsigned>> calls;
 
 	auto compare = [&](unsigned _a, unsigned _b) {
-		return _graph.nodes.at(_a).name > _graph.nodes.at(_b).name;
+		auto extract = [&](string const& _s) {
+			// We want to sort sibling predicates in the counterexample graph by their unique predicate id.
+			// For most predicates, this actually doesn't matter.
+			// The cases where this matters are internal and external function calls which have the form:
+			// summary_<CALLID>_<suffix>
+			// nondet_call_<CALLID>_<suffix>
+			// Those have the extra unique <CALLID> numbers based on the traversal order, and are necessary
+			// to infer the call order so that's shown property in the counterexample trace.
+			// Predicates that do not have a CALLID have a predicate id at the end of <suffix>,
+			// so the assertion below should still hold.
+			auto beg = _s.data();
+			while (beg != _s.data() + _s.size() && !isdigit(*beg)) ++beg;
+			auto end = beg;
+			while (end != _s.data() + _s.size() && isdigit(*end)) ++end;
+
+			solAssert(beg != end, "Expected to find numerical call or predicate id.");
+
+			int result;
+			auto [p, ec] = std::from_chars(beg, end, result);
+			solAssert(ec == std::errc(), "Id should be a number.");
+
+			return result;
+		};
+		return extract(_graph.nodes.at(_a).name) > extract(_graph.nodes.at(_b).name);
 	};
 
 	queue<pair<unsigned, unsigned>> q;
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol
index 7e45e8cd4..c7b8dee56 100644
--- a/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol
+++ b/test/libsolidity/smtCheckerTests/abi/abi_encode_array_slice_2.sol
@@ -8,10 +8,12 @@ contract C {
 
 		bytes memory b3 = abi.encode(data[:data.length]);
 		// should hold but the engine cannot infer that data is fully equals data[:data.length] because each index is assigned separately
-		assert(b1.length == b3.length); // fails for now
+		// Disabled because of Spacer nondeterminism.
+		//assert(b1.length == b3.length); // fails for now
 
 		bytes memory b4 = abi.encode(data[5:10]);
-		assert(b1.length == b4.length); // should fail
+		// Disabled because of Spacer nondeterminism.
+		//assert(b1.length == b4.length); // should fail
 
 		uint x = 5;
 		uint y = 10;
@@ -20,14 +22,10 @@ contract C {
 		assert(b1.length == b5.length); // fails for now
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
+// Warning 2072: (364-379): Unused local variable.
+// Warning 2072: (650-665): Unused local variable.
 // Warning 6328: (312-342): CHC: Assertion violation happens here.
-// Warning 1218: (548-578): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (548-578): CHC: Assertion violation might happen here.
-// Warning 1218: (644-674): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (644-674): CHC: Assertion violation might happen here.
-// Warning 1218: (895-925): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (895-925): CHC: Assertion violation might happen here.
-// Warning 4661: (548-578): BMC: Assertion violation happens here.
-// Warning 4661: (644-674): BMC: Assertion violation happens here.
-// Warning 4661: (895-925): BMC: Assertion violation happens here.
+// Warning 6328: (995-1025): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
index fa32f6d3f..4cd94ef6c 100644
--- a/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
+++ b/test/libsolidity/smtCheckerTests/blockchain_state/transfer.sol
@@ -10,4 +10,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 39\n\nTransaction trace:\nC.constructor()\nC.f(39)
+// Warning 6328: (199-234): CHC: Assertion violation happens here.\nCounterexample:\n\na = 21238\n\nTransaction trace:\nC.constructor()\nC.f(21238)
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol
index b9dc9f051..d5d75fe54 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol
@@ -25,4 +25,4 @@ contract D is C {
 	}
 }
 // ----
-// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 1\n\nTransaction trace:\nD.constructor(1)
+// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\na = 0\n\nTransaction trace:\nD.constructor(0)
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
index 89a01baaa..17e5d297c 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol
@@ -19,17 +19,17 @@ contract C {
 	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);
 		address a1 = ecrecover(h1, v1, r1, s1);
-		assert(a0 == a1);
+		// Disabled because of Spacer nondeterminism.
+		//assert(a0 == a1);
 	}
 }
 // ====
 // SMTIgnoreCex: yes
 // ----
+// Warning 2072: (589-599): Unused local variable.
+// Warning 2072: (631-641): Unused local variable.
 // Warning 1218: (168-184): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (168-184): CHC: Assertion violation might happen here.
 // Warning 6328: (305-321): CHC: Assertion violation happens here.
-// Warning 1218: (448-464): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (448-464): CHC: Assertion violation might happen here.
-// Warning 6328: (673-689): CHC: Assertion violation happens here.
+// Warning 6328: (448-464): CHC: Assertion violation happens here.
 // Warning 4661: (168-184): BMC: Assertion violation happens here.
-// Warning 4661: (448-464): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
index 34c225770..7da246c55 100644
--- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
+++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol
@@ -11,4 +11,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n    C.fi(data, 7719) -- internal call
+// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f(data)\n    C.fi(data, 39) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol b/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
index 3849d4ba2..0ab691148 100644
--- a/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
+++ b/test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol
@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(11)
+// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(9)
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
index efa26f655..0cec4785a 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/nested_arrays_mappings_4.sol
@@ -16,5 +16,7 @@ contract C {
 		assert(y == 1); // should fail
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (293-307): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (293-307): 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 69a1b2a3a..88cc84dd2 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
@@ -19,6 +19,6 @@ contract C {
 }
 // ----
 // Warning 7737: (116-182): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
-// Warning 6328: (185-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
+// Warning 6328: (185-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 43\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
 // Warning 6328: (219-233): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f()
 // Warning 7737: (116-182): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).
diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol
index 998564406..b4d17d235 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol
@@ -15,4 +15,4 @@ contract C
 // SMTSolvers: z3
 // ----
 // Warning 5740: (120-123): Unreachable code.
-// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)
+// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\nTransaction trace:\nC.constructor()\nC.f(3)
diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
index feecd7a9a..31334a72b 100644
--- a/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
+++ b/test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol
@@ -7,4 +7,4 @@ contract C  {
 }
 // ----
 // Warning 4281: (110-115): CHC: Division by zero happens here.\nCounterexample:\n\nx = 0\ny = 0\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
-// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))
+// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
index bfbe68e85..6cc22cf69 100644
--- a/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
+++ b/test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol
@@ -14,6 +14,6 @@ contract C {
 // Warning 2072: (184-188): Unused local variable.
 // Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
 // Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
-// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]\n\nTransaction trace:\nC.constructor()\nC.f([10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10])
+// Warning 6328: (252-268): 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]\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 8364: (155-156): Assertion checker does not yet implement type type(contract C)
 // Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol
index d3ca19baf..de89e01cb 100644
--- a/test/libsolidity/smtCheckerTests/special/difficulty.sol
+++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol
@@ -7,4 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 39\n\nTransaction trace:\nC.constructor()\nC.f(39)
+// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 38\n\nTransaction trace:\nC.constructor()\nC.f(38)
diff --git a/test/libsolidity/smtCheckerTests/special/event.sol b/test/libsolidity/smtCheckerTests/special/event.sol
index 824baa751..21a63fc05 100644
--- a/test/libsolidity/smtCheckerTests/special/event.sol
+++ b/test/libsolidity/smtCheckerTests/special/event.sol
@@ -27,4 +27,4 @@ contract C {
 // ----
 // Warning 6321: (280-284): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
 // Warning 6321: (430-434): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
-// Warning 6328: (440-449): 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: (440-449): 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/this.sol b/test/libsolidity/smtCheckerTests/special/this.sol
index 5bcf81ef8..56826fe64 100644
--- a/test/libsolidity/smtCheckerTests/special/this.sol
+++ b/test/libsolidity/smtCheckerTests/special/this.sol
@@ -7,4 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (85-111): CHC: Assertion violation happens here.\nCounterexample:\n\na = 1\n\nTransaction trace:\nC.constructor()\nC.f(1)
+// Warning 6328: (85-111): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(0)
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol
index 8375aff96..1ab45c907 100644
--- a/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol
@@ -14,4 +14,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (250-294): CHC: Assertion violation happens here.
+// Warning 6328: (250-294): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()\n    C.g() -- trusted external call
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
index 86bdf1569..49f0d6b40 100644
--- a/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol
@@ -12,4 +12,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21238\n\nTransaction trace:\nc.constructor()\nc.g(38, 21238)\n    c.f(map, 38, 21238) -- internal call
+// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\nTransaction trace:\nc.constructor()\nc.g(38, 21239)\n    c.f(map, 38, 21239) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol
index 53b8e5941..7c9e79b2c 100644
--- a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol
@@ -9,4 +9,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (119-133): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 0)
+// Warning 6328: (119-133): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.f(0, 1)
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol
index b8dd609ee..00b79fe2b 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_4.sol
@@ -17,6 +17,8 @@ contract C {
 		assert(s1.x == 44 || s2.x == 44);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
 // Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
@@ -51,9 +53,9 @@ contract C {
 // Warning 8364: (366-368): Assertion checker does not yet implement type struct C.S storage ref
 // Warning 7650: (380-384): Assertion checker does not yet support this expression.
 // Warning 8364: (380-382): Assertion checker does not yet implement type struct C.S storage ref
-// Warning 6328: (197-233): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = false\nb2 = false\n\nTransaction trace:\nC.constructor()\nC.f(false, false)
-// Warning 6328: (237-273): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = false\nb2 = false\n\nTransaction trace:\nC.constructor()\nC.f(false, false)
-// Warning 6328: (359-391): CHC: Assertion violation happens here.\nCounterexample:\n\nb1 = false\nb2 = false\n\nTransaction trace:\nC.constructor()\nC.f(false, false)
+// Warning 6328: (197-233): CHC: Assertion violation happens here.
+// Warning 6328: (237-273): CHC: Assertion violation happens here.
+// Warning 6328: (359-391): CHC: Assertion violation happens here.
 // Warning 8115: (81-85): Assertion checker does not yet support the type of this variable.
 // Warning 8115: (88-92): Assertion checker does not yet support the type of this variable.
 // Warning 8115: (135-147): Assertion checker does not yet support the type of this variable.