diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol
index 3d513a34e..b75510a58 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol
@@ -37,6 +37,8 @@ contract C {
 		assert(owner == address(0) || y != z);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (435-461): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 0, y = 0, z = 0, s = 0\nf()
-// Warning 6328: (594-631): CHC: Assertion violation happens here.\nCounterexample:\nowner = 1, y = 0, z = 0, s = 0\n\n\n\nTransaction trace:\nconstructor()\nState: owner = 1, y = 0, z = 0, s = 0\ninv()
+// Warning 6328: (435-461): CHC: Assertion violation happens here.
+// Warning 6328: (594-631): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
index 9f6ce11a8..df0d61f5f 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
@@ -18,5 +18,5 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\nf()
+// Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\ninc()\nState: x = 2, d = 0\nf()
 // Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol b/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol
index db981653d..1e179dcaa 100644
--- a/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol
+++ b/test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol
@@ -7,4 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\na = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 1)
+// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 1\na = 0\n\n\nTransaction trace:\nconstructor()\nf(1, 0)
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol
index d5276972e..50c9ede93 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_state_var_array_pop_1.sol
@@ -20,6 +20,8 @@ contract C {
 		s.a.pop();
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 2529: (121-130): CHC: Empty array "pop" happens here.\nCounterexample:\ns = {x: 0, a: []}\n_x = 0\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(0)
-// Warning 6328: (230-254): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 7720, a: [7720, 0]}\n_x = 7720\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 0, a: []}\nf(7720)
+// Warning 2529: (121-130): CHC: Empty array "pop" happens here.
+// Warning 6328: (230-254): CHC: Assertion violation happens here.