From cdfc19b5032d3d9e2e5f77003a379da4bb1ae00b Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Mon, 24 Jul 2023 18:33:43 +0200
Subject: [PATCH] SMTChecker: Bring back counterexample checks in regression
 tests

Since the default is now to ignore the counterexamples when checking
test output, we bring back counterexample checks in tests where the
counterexample is (mostly) deterministic.
---
 .../array_members/pop_1_unsafe.sol            |  1 +
 .../array_members/pop_constructor_unsafe.sol  |  1 +
 .../array_members/push_zero_unsafe.sol        |  3 ++-
 .../control_flow/short_circuit_and_fail.sol   |  3 ++-
 .../short_circuit_and_need_both_fail.sol      |  3 ++-
 .../control_flow/short_circuit_or_fail.sol    |  3 ++-
 .../short_circuit_or_need_both_fail.sol       |  3 ++-
 .../external_calls/call_mutex_unsafe.sol      |  4 ++--
 .../external_calls/external_reentrancy_2.sol  |  3 ++-
 .../underflow_only_in_external_call.sol       |  3 ++-
 .../smtCheckerTests/file_level/easy.sol       |  3 ++-
 .../smtCheckerTests/file_level/struct.sol     |  5 +++--
 .../functions/functions_identity_1_fail.sol   |  1 +
 .../functions/functions_identity_2_fail.sol   |  1 +
 .../functions/getters/array_2.sol             |  4 ++--
 .../functions/getters/array_of_structs_2.sol  |  3 ++-
 .../functions/getters/mapping_1.sol           |  3 ++-
 .../functions/getters/mapping_2.sol           |  3 ++-
 .../functions/getters/struct_1.sol            |  3 ++-
 .../functions/getters/struct_2.sol            |  3 ++-
 .../getters/struct_with_reassignment.sol      |  5 +++--
 .../functions/getters/uint.sol                |  3 ++-
 .../functions/super_function_assert.sol       |  5 +++--
 .../base_contract_assertion_fail_1.sol        |  3 ++-
 .../base_contract_assertion_fail_2.sol        |  3 ++-
 .../base_contract_assertion_fail_3.sol        |  3 ++-
 .../base_contract_assertion_fail_4.sol        |  3 ++-
 .../base_contract_assertion_fail_5.sol        |  3 ++-
 .../base_contract_assertion_fail_6.sol        |  3 ++-
 .../base_contract_assertion_fail_7.sol        |  3 ++-
 .../base_contract_assertion_fail_8.sol        |  1 +
 .../base_contract_assertion_fail_9.sol        |  5 +++--
 .../inheritance/diamond_super_1.sol           |  3 ++-
 .../inheritance/diamond_super_2.sol           |  5 +++--
 .../inheritance/diamond_super_3.sol           |  3 ++-
 .../loops/while_loop_simple_1.sol             |  1 +
 .../assignment_chain_tuple_contract_2.sol     |  5 ++++-
 .../assignment_chain_tuple_contract_3.sol     |  7 ++++--
 .../operators/bitwise_and_int.sol             | 11 +++++-----
 .../operators/shifts/shift_cex.sol            | 22 +++++++++++++++++++
 .../smtCheckerTests/operators/unary_add.sol   |  3 ++-
 .../smtCheckerTests/operators/unary_sub.sol   |  3 ++-
 .../out_of_bounds/fixed_bytes_2.sol           |  1 +
 .../smtCheckerTests/simple/cex_smoke_test.sol | 12 ++++++++++
 .../smtCheckerTests/try_catch/try_3.sol       |  3 ++-
 .../smtCheckerTests/types/array_literal_2.sol |  3 ++-
 .../smtCheckerTests/types/array_literal_3.sol |  1 +
 .../smtCheckerTests/types/array_literal_5.sol |  3 ++-
 .../smtCheckerTests/types/array_literal_6.sol |  5 +++--
 .../smtCheckerTests/types/bool_simple_1.sol   |  1 +
 .../smtCheckerTests/types/mapping_1_fail.sol  |  1 +
 .../struct/struct_constructor_named_args.sol  |  3 ++-
 .../smtCheckerTests/types/tuple_function.sol  |  1 +
 .../types/tuple_function_2.sol                |  3 ++-
 .../types/tuple_function_3.sol                |  5 +++--
 .../smtCheckerTests/userTypes/constant.sol    |  3 ++-
 56 files changed, 147 insertions(+), 57 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/shifts/shift_cex.sol
 create mode 100644 test/libsolidity/smtCheckerTests/simple/cex_smoke_test.sol

diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
index 270fa28fb..833983469 100644
--- a/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_1_unsafe.sol
@@ -6,5 +6,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 2529: (49-56): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
index 1cb1ed013..7e1eb8b69 100644
--- a/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/pop_constructor_unsafe.sol
@@ -6,5 +6,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 2529: (43-50): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\n\nTransaction trace:\nC.constructor()
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
index aab7b5b78..ed846fae0 100644
--- a/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol
@@ -7,6 +7,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (61-91): CHC: Assertion violation happens here.
+// Warning 6328: (61-91): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
index 0935d29c6..a38ffdf8a 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_fail.sol
@@ -14,6 +14,7 @@ contract c {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (194-203): CHC: Assertion violation happens here.
+// Warning 6328: (194-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\nb = false\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n    c.f() -- internal call\n    c.f() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
index d21d8e041..a5337675e 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_and_need_both_fail.sol
@@ -14,6 +14,7 @@ contract c {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (192-202): CHC: Assertion violation happens here.
+// Warning 6328: (192-202): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n    c.f() -- internal call\n    c.f() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
index 8ac219ae5..c60dcc113 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_fail.sol
@@ -14,6 +14,7 @@ contract c {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (192-202): CHC: Assertion violation happens here.
+// Warning 6328: (192-202): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n    c.f() -- internal call\n    c.f() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
index ea71f34b0..e528cf49d 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/short_circuit_or_need_both_fail.sol
@@ -14,6 +14,7 @@ contract c {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (192-202): CHC: Assertion violation happens here.
+// Warning 6328: (192-202): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n = false\nb = true\n\nTransaction trace:\nc.constructor()\nState: x = 0\nc.g()\n    c.f() -- internal call\n    c.f() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
index 64494971a..e8c17d3eb 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
@@ -21,7 +21,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreCex: yes
+// SMTIgnoreCex: no
 // ----
 // Warning 9302: (212-228): Return value of low-level calls not used.
-// Warning 6328: (232-246): CHC: Assertion violation happens here.
+// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, lock = false\n_a = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.set(1)\nState: x = 1, lock = false\nC.f(0x0)\n    _a.call("aaaaa") -- untrusted external call, synthesized as:\n        C.set(0) -- reentrant call
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
index 268db82b4..1783be781 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
@@ -12,5 +12,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (117-131): CHC: Assertion violation happens here.
+// Warning 6328: (117-131): CHC: Assertion violation happens here.\nCounterexample:\nlocked = false\ntarget = 0x0\n\nTransaction trace:\nC.constructor()\nState: locked = true\nC.call(0x0)\n    D(target).e() -- untrusted external call, synthesized as:\n        C.call(0x0) -- reentrant call
diff --git a/test/libsolidity/smtCheckerTests/external_calls/underflow_only_in_external_call.sol b/test/libsolidity/smtCheckerTests/external_calls/underflow_only_in_external_call.sol
index a0c3a06b4..0b5c8fa07 100644
--- a/test/libsolidity/smtCheckerTests/external_calls/underflow_only_in_external_call.sol
+++ b/test/libsolidity/smtCheckerTests/external_calls/underflow_only_in_external_call.sol
@@ -18,6 +18,7 @@ contract C {
 }
 // ====
 // SMTEngine: chc
+// SMTIgnoreCex: no
 // SMTTargets: underflow
 // ----
-// Warning 3944: (109-112): CHC: Underflow (resulting value less than 0) happens here.
+// Warning 3944: (109-112): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nv = 0, guard = false\n = 0\n\nTransaction trace:\nC.constructor()\nState: v = 0, guard = true\nC.f()\n    C.dec() -- trusted external call
diff --git a/test/libsolidity/smtCheckerTests/file_level/easy.sol b/test/libsolidity/smtCheckerTests/file_level/easy.sol
index 07ad9f079..2cbef3f5c 100644
--- a/test/libsolidity/smtCheckerTests/file_level/easy.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/easy.sol
@@ -13,6 +13,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (222-239): CHC: Assertion violation happens here.
+// Warning 6328: (222-239): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f(7) -- internal call\n        add(7, 2) -- internal call\n    C.f(8) -- internal call\n        add(8, 2) -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/file_level/struct.sol b/test/libsolidity/smtCheckerTests/file_level/struct.sol
index 664e1ac5f..f469933db 100644
--- a/test/libsolidity/smtCheckerTests/file_level/struct.sol
+++ b/test/libsolidity/smtCheckerTests/file_level/struct.sol
@@ -22,7 +22,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (317-333): CHC: Assertion violation happens here.
-// Warning 6328: (352-371): CHC: Assertion violation happens here.
+// Warning 6328: (317-333): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 2, a: [1]}\n\nTransaction trace:\nC.constructor()\nC.f()\n    allocate(2, 1) -- internal call
+// Warning 6328: (352-371): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 2, a: [1]}\n\nTransaction trace:\nC.constructor()\nC.f()\n    allocate(2, 1) -- internal call
 // Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
index ceb42881f..414a8a52b 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol
@@ -11,5 +11,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 6328: (129-142): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.h(0) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
index 4d6ff0a64..955f6906c 100644
--- a/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
+++ b/test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol
@@ -15,5 +15,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 6328: (197-210): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.h(0) -- internal call\n        C.k(0) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
index 3c9fc7eb8..2d92413d5 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/array_2.sol
@@ -17,7 +17,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreCex: yes
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (242-256): CHC: Assertion violation happens here.
+// Warning 6328: (242-256): CHC: Assertion violation happens here.\nCounterexample:\na = [[], [], [0, 0, 0, 0]]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [[], [], [0, 0, 0, 0]]\nC.f()
 // Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol
index 36ea9da2f..b62611b51 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/array_of_structs_2.sol
@@ -18,6 +18,7 @@ contract D {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (267-281): CHC: Assertion violation happens here.
+// Warning 6328: (267-281): CHC: Assertion violation happens here.\nCounterexample:\nitems = [{x: 42, y: 43}]\na = 42\nb = 43\n\nTransaction trace:\nD.constructor()\nState: items = []\nD.test()
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol
index 1077c2ee2..4dbd6a489 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_1.sol
@@ -9,6 +9,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (142-156): CHC: Assertion violation happens here.
+// Warning 6328: (142-156): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol
index c97084164..418515a20 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/mapping_2.sol
@@ -9,6 +9,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (166-180): CHC: Assertion violation happens here.
+// Warning 6328: (166-180): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol
index 521f108e0..06c021706 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_1.sol
@@ -26,6 +26,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (338-355): CHC: Assertion violation happens here.
+// Warning 6328: (338-355): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 0, t: {t: 0}, b: false, a: []}\ny = 0\nc = false\nt = {t: 0}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0, t: {t: 0}, b: false, a: []}\nC.f()
 // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol
index eec69480a..b43df21fc 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_2.sol
@@ -16,6 +16,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (175-189): CHC: Assertion violation happens here.
+// Warning 6328: (175-189): CHC: Assertion violation happens here.\nCounterexample:\ns = {a: [0, 0], u: 0}\nu = 0\n\nTransaction trace:\nC.constructor()\nState: s = {a: [0, 0], u: 0}\nC.f()
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol b/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol
index 4f4f8e13c..a322f4fb4 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/struct_with_reassignment.sol
@@ -27,7 +27,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (255-272): CHC: Assertion violation happens here.
-// Warning 6328: (377-391): CHC: Assertion violation happens here.
+// Warning 6328: (255-272): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 1, b: false}\nx = 1\nb = false\ny = 0\nc = false\n\nTransaction trace:\nC.constructor()\nState: s = {x: 1, b: false}\nC.f()
+// Warning 6328: (377-391): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42, b: false}\nx = 1\nb = false\ny = 42\nc = false\n\nTransaction trace:\nC.constructor()\nState: s = {x: 1, b: false}\nC.f()
 // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/uint.sol b/test/libsolidity/smtCheckerTests/functions/getters/uint.sol
index 35a781dd7..d05753dd7 100644
--- a/test/libsolidity/smtCheckerTests/functions/getters/uint.sol
+++ b/test/libsolidity/smtCheckerTests/functions/getters/uint.sol
@@ -9,6 +9,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (114-128): CHC: Assertion violation happens here.
+// Warning 6328: (114-128): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol
index 3bec690e6..e0b191573 100644
--- a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol
+++ b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol
@@ -28,7 +28,8 @@ contract D is C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (205-219): CHC: Assertion violation happens here.
-// Warning 6328: (328-342): CHC: Assertion violation happens here.
+// Warning 6328: (205-219): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.proxy()\n    C.f() -- internal call\n        A.f() -- internal call
+// Warning 6328: (328-342): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()\nState: x = 0\nA.proxy()\n    D.f() -- internal call\n        C.f() -- internal call\n            A.f() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
index 587a23bb0..6ecfed791 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol
@@ -14,6 +14,7 @@ contract C is B {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (52-66): CHC: Assertion violation happens here.
+// Warning 6328: (52-66): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n    B.f() -- internal call
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol
index 97c79428b..85e2677f7 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol
@@ -21,6 +21,7 @@ contract C is B {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (54-68): CHC: Assertion violation happens here.
+// Warning 6328: (54-68): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, z = 0, w = 0, a = 0, b = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, z = 0, w = 0, a = 0, b = 0, x = 0\nC.g()\n    A.f() -- internal call
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_3.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_3.sol
index c92b0c501..f1481197f 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_3.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_3.sol
@@ -27,6 +27,7 @@ contract C is B {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (64-78): CHC: Assertion violation happens here.
+// Warning 6328: (64-78): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    B.f() -- internal call\n        A.f() -- internal call\n            C.v() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_4.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_4.sol
index 593a6ba3a..04b7ea748 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_4.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_4.sol
@@ -34,6 +34,7 @@ contract C is B, A1 {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (64-78): CHC: Assertion violation happens here.
+// Warning 6328: (64-78): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    C.f() -- internal call\n        A1.f() -- internal call\n            B.f() -- internal call\n                A.f() -- internal call\n                    C.v() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_5.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_5.sol
index 818906cd3..e386c4b44 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_5.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_5.sol
@@ -28,6 +28,7 @@ contract C is B {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (97-111): CHC: Assertion violation happens here.
+// Warning 6328: (97-111): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    B.f() -- internal call\n        A.f() -- internal call\n            C.v() -- internal call\n                A.v() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_6.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_6.sol
index 04033a00f..2bac9303b 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_6.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_6.sol
@@ -30,6 +30,7 @@ contract C is B {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (183-197): CHC: Assertion violation happens here.
+// Warning 6328: (183-197): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()\n    A.v() -- internal call
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_7.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_7.sol
index e33e6a3bc..45cf7fe18 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_7.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_7.sol
@@ -21,6 +21,7 @@ contract C is A {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (56-70): CHC: Assertion violation happens here.
+// Warning 6328: (56-70): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    A.f() -- internal call\n        C.v() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol
index a326ccf3b..068531b44 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol
@@ -14,5 +14,6 @@ contract C is  A {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 6328: (61-75): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nA.f()
diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
index 2ec47f7d9..9972c7e3f 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol
@@ -27,7 +27,8 @@ contract C is B {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (62-76): CHC: Assertion violation happens here.
-// Warning 6328: (131-145): CHC: Assertion violation happens here.
+// Warning 6328: (62-76): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nB.f()\n    A.f() -- internal call\n        C.v() -- internal call
+// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n    A.v() -- internal call
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_1.sol b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_1.sol
index 7af69f2e4..546f934b7 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_1.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_1.sol
@@ -28,6 +28,7 @@ contract D is B, C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (437-452): CHC: Assertion violation happens here.
+// Warning 6328: (437-452): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 15\n\nTransaction trace:\nD.constructor()\nD.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call
 // Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_2.sol b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_2.sol
index c5f838397..1825098a8 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_2.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_2.sol
@@ -29,7 +29,8 @@ contract D is B, C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (443-458): CHC: Assertion violation happens here.
-// Warning 6328: (477-492): CHC: Assertion violation happens here.
+// Warning 6328: (443-458): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 22\n\nTransaction trace:\nD.constructor()\nD.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call
+// Warning 6328: (477-492): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 22\n\nTransaction trace:\nD.constructor()\nD.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call
 // Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
index af22069eb..f6674021e 100644
--- a/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
+++ b/test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol
@@ -31,6 +31,7 @@ contract E is C,D {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (379-394): CHC: Assertion violation happens here.
+// Warning 6328: (379-394): CHC: Assertion violation happens here.\nCounterexample:\nx = 111\n\nTransaction trace:\nE.constructor()\nState: x = 0\nE.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call
 // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol
index 59edfb55b..461e4f4e6 100644
--- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol
+++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_1.sol
@@ -11,5 +11,6 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTSolvers: z3
+// SMTIgnoreCex: no
 // ----
 // Warning 6328: (162-176): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f(0)
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol
index 461761baf..c89314e0f 100644
--- a/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol
+++ b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_2.sol
@@ -9,6 +9,9 @@ contract C {
         assert(x != 2); // should fail
     }
 }
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (174-188): CHC: Assertion violation happens here.
+// Warning 6328: (174-188): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 2\nC.g()
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol
index 6496ec525..e53436a0f 100644
--- a/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol
+++ b/test/libsolidity/smtCheckerTests/operators/assignment_chain_tuple_contract_3.sol
@@ -17,7 +17,10 @@ contract D is C {
         assert(y == 3); // should hold
     }
 }
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (95-109): CHC: Assertion violation happens here.
-// Warning 6328: (180-194): CHC: Assertion violation happens here.
+// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\ny = 3, x = 3\n\nTransaction trace:\nD.constructor()\nState: y = 3, x = 3\nC.f()
+// Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 2\nC.g()
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol
index 4bae4f67b..b280038ac 100644
--- a/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_and_int.sol
@@ -2,18 +2,19 @@ contract C {
 	function f() public pure {
 		int8 x = 1;
 		int8 y = 0;
-		assert(x & y != 0);
+		assert(x & y != 0); // should fail
 		x = -1; y = 3;
-		assert(x & y == 3);
+		assert(x & y == 3); // should hold
 		y = -1;
 		int8 z = x & y;
-		assert(z == -1);
+		assert(z == -1); // should hold
 		y = 127;
-		assert(x & y == 127);
+		assert(x & y == 127); // should hold
 	}
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (71-89): CHC: Assertion violation happens here.
+// Warning 6328: (71-89): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\nz = 0\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/shifts/shift_cex.sol b/test/libsolidity/smtCheckerTests/operators/shifts/shift_cex.sol
new file mode 100644
index 000000000..8670b79c0
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/shifts/shift_cex.sol
@@ -0,0 +1,22 @@
+contract C {
+	function left() public pure {
+		uint x = 0x4266;
+		assert(x << 0x0 == 0x4266);
+		// Fails because the above is true.
+		assert(x << 0x0 == 0x4268);
+	}
+
+	function right() public pure {
+		uint x = 0x4266;
+		assert(x >> 0x0 == 0x4266);
+		// Fails because the above is true.
+		assert(x >> 0x0 == 0x4268);
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: no
+// ----
+// Warning 6328: (133-159): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16998\n\nTransaction trace:\nC.constructor()\nC.left()
+// Warning 6328: (286-312): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 16998\n\nTransaction trace:\nC.constructor()\nC.right()
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add.sol b/test/libsolidity/smtCheckerTests/operators/unary_add.sol
index 9716624b2..571cd666c 100644
--- a/test/libsolidity/smtCheckerTests/operators/unary_add.sol
+++ b/test/libsolidity/smtCheckerTests/operators/unary_add.sol
@@ -13,6 +13,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (161-174): CHC: Assertion violation happens here.
+// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 4\na = 3\nb = 3\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/operators/unary_sub.sol b/test/libsolidity/smtCheckerTests/operators/unary_sub.sol
index adf70fe42..86ec98062 100644
--- a/test/libsolidity/smtCheckerTests/operators/unary_sub.sol
+++ b/test/libsolidity/smtCheckerTests/operators/unary_sub.sol
@@ -13,6 +13,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (161-174): CHC: Assertion violation happens here.
+// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\na = 4\nb = 4\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol
index f4e90ddb7..d51685f39 100644
--- a/test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol
+++ b/test/libsolidity/smtCheckerTests/out_of_bounds/fixed_bytes_2.sol
@@ -5,5 +5,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 6368: (83-87): CHC: Out of bounds access happens here.\nCounterexample:\n\nx = 0x0\ny = 4\n = 0x0\n\nTransaction trace:\nC.constructor()\nC.r(0x0, 4)
diff --git a/test/libsolidity/smtCheckerTests/simple/cex_smoke_test.sol b/test/libsolidity/smtCheckerTests/simple/cex_smoke_test.sol
new file mode 100644
index 000000000..a59233103
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/simple/cex_smoke_test.sol
@@ -0,0 +1,12 @@
+contract C {
+
+    function f() public pure {
+        uint x = 1;
+        assert(x == 2);
+    }
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (73-87): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\nTransaction trace:\nC.constructor()\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_3.sol b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol
index 77e53f860..7698eed0f 100644
--- a/test/libsolidity/smtCheckerTests/try_catch/try_3.sol
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol
@@ -21,7 +21,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 5667: (259-273): Unused try/catch parameter. Remove or comment out the variable name to silence this warning.
-// Warning 6328: (280-294): CHC: Assertion violation happens here.
+// Warning 6328: (280-294): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\ns = []\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n    C.postinc() -- internal call
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_2.sol b/test/libsolidity/smtCheckerTests/types/array_literal_2.sol
index 1136a9d1f..d48644c2f 100644
--- a/test/libsolidity/smtCheckerTests/types/array_literal_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_literal_2.sol
@@ -10,6 +10,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (167-187): CHC: Assertion violation happens here.
+// Warning 6328: (167-187): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4]\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_3.sol b/test/libsolidity/smtCheckerTests/types/array_literal_3.sol
index 52baec977..cdaff2bf4 100644
--- a/test/libsolidity/smtCheckerTests/types/array_literal_3.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_literal_3.sol
@@ -9,6 +9,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 6328: (168-188): CHC: Assertion violation happens here.
 // Info 1391: CHC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_5.sol b/test/libsolidity/smtCheckerTests/types/array_literal_5.sol
index 7c4c9d3d9..0a6fe02bc 100644
--- a/test/libsolidity/smtCheckerTests/types/array_literal_5.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_literal_5.sol
@@ -12,6 +12,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (176-196): CHC: Assertion violation happens here.
+// Warning 6328: (176-196): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f()
 // Info 1391: CHC: 9 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/array_literal_6.sol b/test/libsolidity/smtCheckerTests/types/array_literal_6.sol
index e612b08a2..b017aa93e 100644
--- a/test/libsolidity/smtCheckerTests/types/array_literal_6.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_literal_6.sol
@@ -13,7 +13,8 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (146-174): CHC: Assertion violation happens here.
-// Warning 6328: (235-255): CHC: Assertion violation happens here.
+// Warning 6328: (146-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nC.f()
+// Warning 6328: (235-255): CHC: Assertion violation happens here.\nCounterexample:\n\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1391: CHC: 11 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/bool_simple_1.sol b/test/libsolidity/smtCheckerTests/types/bool_simple_1.sol
index 52b05f3bd..a9ea6c7f9 100644
--- a/test/libsolidity/smtCheckerTests/types/bool_simple_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/bool_simple_1.sol
@@ -5,5 +5,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 6328: (58-67): CHC: Assertion violation happens here.\nCounterexample:\n\nx = false\n\nTransaction trace:\nC.constructor()\nC.f(false)
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol b/test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol
index d72f62be9..7e9669eaf 100644
--- a/test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol
+++ b/test/libsolidity/smtCheckerTests/types/mapping_1_fail.sol
@@ -9,5 +9,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 6328: (101-120): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\nTransaction trace:\nC.constructor()\nC.f(3)
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol
index b12882ef7..d52a71697 100644
--- a/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol
+++ b/test/libsolidity/smtCheckerTests/types/struct/struct_constructor_named_args.sol
@@ -19,6 +19,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (232-255): CHC: Assertion violation happens here.
+// Warning 6328: (232-255): CHC: Assertion violation happens here.\nCounterexample:\n\ninner = {x: 43}\nouter = {s: {x: 43}, y: 512}\n\nTransaction trace:\nC.constructor()\nC.test()
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function.sol b/test/libsolidity/smtCheckerTests/types/tuple_function.sol
index ef3ad0102..97156f5cf 100644
--- a/test/libsolidity/smtCheckerTests/types/tuple_function.sol
+++ b/test/libsolidity/smtCheckerTests/types/tuple_function.sol
@@ -13,6 +13,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
 // Warning 6328: (149-163): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call
 // Warning 6328: (167-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol b/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol
index 362755ac9..62b73e904 100644
--- a/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol
+++ b/test/libsolidity/smtCheckerTests/types/tuple_function_2.sol
@@ -13,6 +13,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (166-180): CHC: Assertion violation happens here.
+// Warning 6328: (166-180): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 0\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol b/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol
index f33f9bfc8..0e0c7bded 100644
--- a/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol
+++ b/test/libsolidity/smtCheckerTests/types/tuple_function_3.sol
@@ -15,7 +15,8 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (172-186): CHC: Assertion violation happens here.
-// Warning 6328: (190-204): CHC: Assertion violation happens here.
+// Warning 6328: (172-186): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\nb = false\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call
+// Warning 6328: (190-204): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 0\nb = false\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call
 // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
diff --git a/test/libsolidity/smtCheckerTests/userTypes/constant.sol b/test/libsolidity/smtCheckerTests/userTypes/constant.sol
index 0d49dec4b..baba50d07 100644
--- a/test/libsolidity/smtCheckerTests/userTypes/constant.sol
+++ b/test/libsolidity/smtCheckerTests/userTypes/constant.sol
@@ -14,6 +14,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: no
 // ----
-// Warning 6328: (531-555): CHC: Assertion violation happens here.
+// Warning 6328: (531-555): CHC: Assertion violation happens here.\nCounterexample:\nu = 165521356710917456517261742455526507355687727119203895813322792776\n\nTransaction trace:\nC.constructor()\nState: u = 165521356710917456517261742455526507355687727119203895813322792776\nC.f()
 // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.