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