Merge pull request #12521 from ethereum/smt_z3_4_14

ekpyron · web-flow · commit 81d3e532b8e9 · 2022-01-12T19:26:03.000+01:00
update smtchecker tests for new z3
diff --git a/.circleci/config.yml b/.circleci/config.yml
@@ -9,20 +9,20 @@ version: 2.1
 parameters:
   ubuntu-2004-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-9
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:3d8a912e8e78e98cd217955d06d98608ad60adc67728d4c3a569991235fa1abb"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-10
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:e61939751ff9777307857361f712b581bfc8a8aaae75fab7b50febc764710587"
   ubuntu-2004-clang-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-9
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:a1ba002cae17279d1396a898b04e4e9c45602ad881295db3e2f484a7e24f6f43"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-10
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:0de8c68f084120b2a165406e3a0c2aab58b32f5b7182c2322245245f1d243b8d"
   ubuntu-1604-clang-ossfuzz-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-14
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:f353823cce2f6cd2f9f1459d86cd76fdfc551a0261d87626615ea6c1d8f90587"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-15
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:87f1a57586eec194a6217ab624efc69d3d9af2f7ac8ca36497ad57488c2f08ae"
   emscripten-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:emscripten-8
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:842d6074e0e7e5355c89122c1cafc1fdb59696596750e7d56e5f35c0d883ad59"
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-9
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24"
   evm-version:
     type: string
     default: london
diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh
@@ -61,11 +61,11 @@ then
   ./scripts/install_obsolete_jsoncpp_1_7_4.sh
 
   # z3
-  z3_version="4.8.13"
+  z3_version="4.8.14"
   z3_dir="z3-${z3_version}-x64-osx-10.16"
   z3_package="${z3_dir}.zip"
   wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}"
-  validate_checksum "$z3_package" 191b26be2b617b2dffffce139d77abcd7e584859efbc10a58d01a1d7830697a4
+  validate_checksum "$z3_package" 1341671670e0c4e72da80815128a68975ee90816d50ceaf6bd820f06babe2cfd
   unzip "$z3_package"
   rm "$z3_package"
   cp "${z3_dir}/bin/libz3.a" /usr/local/lib
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -65,7 +65,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
 
 include(EthOptions)
 configure_project(TESTS)
-set(LATEST_Z3_VERSION "4.8.13")
+set(LATEST_Z3_VERSION "4.8.14")
 set(MINIMUM_Z3_VERSION "4.8.0")
 find_package(Z3)
 if (${Z3_FOUND})
diff --git a/scripts/build_emscripten.sh b/scripts/build_emscripten.sh
@@ -34,7 +34,7 @@ else
     BUILD_DIR="$1"
 fi
 
-# solbuildpackpusher/solidity-buildpack-deps:emscripten-8
+# solbuildpackpusher/solidity-buildpack-deps:emscripten-9
 docker run -v "$(pwd):/root/project" -w /root/project \
-    solbuildpackpusher/solidity-buildpack-deps@sha256:842d6074e0e7e5355c89122c1cafc1fdb59696596750e7d56e5f35c0d883ad59 \
+    solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24\
     ./scripts/ci/build_emscripten.sh "$BUILD_DIR"
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_2.sol
@@ -14,7 +14,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 28100 }\nState: x = 115792089237316195423570985008687907853269984665640564039457584007913129639926, once = false\nC.f(){ msg.value: 8 }
-// Warning 6328: (235-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, once = true\n\nTransaction trace:\nC.constructor(){ msg.value: 0 }\nState: x = 0, once = false\nC.f(){ msg.value: 8 }
+// Warning 4984: (266-272): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (235-273): CHC: Assertion violation happens here.
 // Info 1180: Contract invariant(s) for :C:\nonce\n
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_ext_calls_2.sol
@@ -9,7 +9,7 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTIgnoreInv: yes
 // ----
 // Warning 9302: (82-93): Return value of low-level calls not used.
 // Warning 6328: (97-131): CHC: Assertion violation happens here.
-// Info 1180: Reentrancy property(ies) for :C:\n(!(<errorCode> >= 2) && (((:var 1).balances[address(this)] + ((- 1) * (:var 0).balances[address(this)])) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(address(this).balance == x)\n<errorCode> = 2 -> Assertion failed at assert(address(this).balance >= x)\n
diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
@@ -45,5 +45,5 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n    C.reset_if_overflow() -- internal call
-// Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n    C.reset_if_overflow() -- internal call
+// Warning 6328: (502-519): CHC: Assertion violation happens here.
 // Warning 6328: (615-629): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n    C.reset_if_overflow() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol
@@ -21,6 +21,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 9302: (212-228): Return value of low-level calls not used.
-// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n    _a.call("aaaaa") -- untrusted external call, synthesized as:\n        C.set(1) -- reentrant call
+// Warning 6328: (232-246): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol
@@ -12,5 +12,5 @@ contract C {
 // ----
 // Warning 9302: (96-117): Return value of low-level calls not used.
 // Warning 6328: (121-156): CHC: Assertion violation might happen here.
-// Warning 6328: (175-211): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n    i.call{value: 10}("") -- untrusted external call
+// Warning 6328: (175-211): CHC: Assertion violation happens here.
 // Warning 4661: (121-156): BMC: 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
@@ -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 = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
+// 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()
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol
@@ -12,7 +12,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (150-186): CHC: Assertion violation might happen here.
-// Warning 6328: (205-240): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    i.f{value: 0}() -- untrusted external call
+// Warning 6328: (205-240): CHC: Assertion violation happens here.
 // Warning 4661: (150-186): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol
@@ -36,4 +36,4 @@ contract C {
 // SMTIgnoreCex: yes
 // ----
 // Warning 6328: (495-532): CHC: Assertion violation happens here.
-// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) <= 0) && !(<errorCode> = 1) && ((owner + ((- 1) * owner')) >= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n
+// Info 1180: Reentrancy property(ies) for :C:\n(((owner + ((- 1) * owner')) >= 0) && !(<errorCode> = 1) && ((owner + ((- 1) * owner')) <= 0))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(prevOwner == owner)\n<errorCode> = 3 -> Assertion failed at assert(owner == address(0) || y != z)\n
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_3.sol
@@ -40,5 +40,4 @@ contract C {
 }
 // ====
 // SMTEngine: all
-// ----
-// Info 1180: Contract invariant(s) for :C:\n((insidef || (z <= 0)) && (y <= 0))\nReentrancy property(ies) for :C:\n((!insidef || !(<errorCode> >= 2)) && (insidef' || !insidef) && (!(y <= 0) || (y' <= 0)))\n((!insidef || !(<errorCode> >= 3)) && (insidef' || !insidef))\n<errorCode> = 0 -> no errors\n<errorCode> = 2 -> Assertion failed at assert(z == y)\n<errorCode> = 3 -> Assertion failed at assert(prevOwner == owner)\n
+// SMTIgnoreInv: yes
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol
@@ -42,6 +42,9 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTIgnoreOS: macos
 // ----
+// Warning 1218: (437-463): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (419-433): CHC: Assertion violation happens here.
-// Warning 6328: (437-463): CHC: Assertion violation happens here.
+// Warning 6328: (437-463): CHC: Assertion violation might happen here.
+// Warning 4661: (437-463): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
@@ -13,4 +13,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// 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
+// Warning 1218: (117-131): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (117-131): CHC: Assertion violation might happen here.
+// Warning 4661: (117-131): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/file_level/import.sol b/test/libsolidity/smtCheckerTests/file_level/import.sol
@@ -21,6 +21,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 21238}\nx = 8\ny = 21238\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 8}, 8) -- internal call
-// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 6}\nx = 0\ny = 6\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 0}, 8) -- internal call
+// Warning 6328: (B:238-252): CHC: Assertion violation happens here.
+// Warning 6328: (B:308-322): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
@@ -25,4 +25,4 @@ contract C
 // SMTIgnoreOS: macos
 // ----
 // Warning 6328: (234-253): CHC: Assertion violation happens here.
-// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)) && (((map'[1] + ((- 1) * map'[0])) <= 0) || !((map[1] + ((- 1) * map[0])) <= 0)) && !(<errorCode> = 2))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n
+// Info 1180: Reentrancy property(ies) for :C:\n!(<errorCode> = 1)\n((!((map[1] + ((- 1) * map[0])) <= 0) || ((map'[1] + ((- 1) * map'[0])) <= 0)) && !(<errorCode> = 2) && (!((map[1] + ((- 1) * map[0])) >= 0) || ((map'[0] + ((- 1) * map'[1])) <= 0)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 2 -> Assertion failed at assert(map[0] == map[1])\n<errorCode> = 3 -> Assertion failed at assert(map[0] == 0)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol
@@ -27,4 +27,4 @@ contract C is A {
 // ----
 // Warning 6328: (199-214): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i()
 // Warning 6328: (387-401): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i()
-// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x <= 9) && !(x >= 11))\n
+// Info 1180: Contract invariant(s) for :A:\n(!(x <= 1) && !(x >= 3))\nContract invariant(s) for :C:\n(!(x >= 11) && !(x <= 9))\n
diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol
@@ -27,6 +27,6 @@ contract A {
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTIgnoreInv: yes
 // ----
 // Warning 6328: (392-408): CHC: Assertion violation happens here.
-// Info 1180: Contract invariant(s) for :A:\n(((x = (- 2)) && (y = (- 2))) || ((x = 0) && (y = 0)))\n(((x = 0) && (y = 0)) || ((x = (- 2)) && (y = (- 2))))\n
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol b/test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol
@@ -20,4 +20,4 @@ contract C
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [299, 0]\nx = 99\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(99, 0)
+// Warning 6328: (262-284): CHC: Assertion violation happens here.\nCounterexample:\narray = [200, 0]\nx = 0\np = 0\n\nTransaction trace:\nC.constructor()\nState: array = [0, 0]\nC.f(0, 0)
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
@@ -25,4 +25,4 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 2072: (255-261): Unused local variable.
-// Info 1180: Reentrancy property(ies) for :C:\n((!(x <= 2) || !(x' >= 3)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
+// Info 1180: Reentrancy property(ies) for :C:\n((!(x' >= 3) || (a' = a)) && (<errorCode> <= 0) && (!(x' <= 0) || !(x >= 2)) && (!(x <= 2) || !(x' >= 3)))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(x == 2 || x == 1)\n
diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
@@ -13,4 +13,4 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2997\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2803 }\n    _i.f() -- untrusted external call, synthesized as:\n        C.g(0){ msg.value: 32278 } -- reentrant call\n            _i.f() -- untrusted external call
+// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2997\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2803 }\n    _i.f() -- untrusted external call, synthesized as:\n        C.g(0){ msg.value: 2446 } -- reentrant call\n            _i.f() -- untrusted external call
diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_2.sol
@@ -13,4 +13,6 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (157-191): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 101\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 83 }\n    _i.f{ value: 100 }() -- untrusted external call
+// Warning 1218: (157-191): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (157-191): CHC: Assertion violation might happen here.
+// Warning 4661: (157-191): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol
@@ -21,5 +21,5 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (280-300): CHC: Assertion violation happens here.
+// Warning 6328: (280-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.f()
 // Info 1180: Contract invariant(s) for :C:\n!(m[0].length <= 1)\n(!(m[0][1] >= 43) && !(m[0][1] <= 41))\n
diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol
@@ -10,7 +10,8 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (180-204): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0x2297\nb = 0x2297\n\nTransaction trace:\nC.constructor()\nC.f(0x2297, 0x2297)
+// Warning 6328: (180-204): CHC: Assertion violation happens here.
 // Warning 1236: (101-116): BMC: Insufficient funds happens here.
 // Warning 1236: (120-136): BMC: Insufficient funds happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol b/test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol
@@ -8,5 +8,6 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (86-100): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.f(0, 1)
+// Warning 6328: (86-100): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol b/test/libsolidity/smtCheckerTests/types/static_array_length_1.sol
@@ -7,6 +7,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (102-122): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x09, 0x09]\n\nTransaction trace:\nC.constructor()\nC.f([0x09, 0x09])
-// Warning 6328: (141-161): CHC: Assertion violation happens here.\nCounterexample:\n\na = [0x09, 0x09]\n\nTransaction trace:\nC.constructor()\nC.f([0x09, 0x09])
+// Warning 6328: (102-122): CHC: Assertion violation happens here.
+// Warning 6328: (141-161): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol
@@ -20,4 +20,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 10}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 10}\nC.g(){ msg.sender: 0x0985 }
+// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 11}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 11}\nC.g(){ msg.sender: 0x0985 }
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol
@@ -26,4 +26,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g()
+// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 11, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 11, s: {innerM, sum: 21239}}\nC.g()
diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_4.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_4.sol
@@ -25,5 +25,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (305-325): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g()
+// Warning 6328: (305-325): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol b/test/libsolidity/smtCheckerTests/userTypes/fixedpoint.sol

Original file line number	Diff line number	Diff line change
`@@ -21,6 +21,7 @@ contract C {`
`21`	`21`	`}`
`22`	`22`	`// ====`
`23`	`23`	`// SMTEngine: all`
	`24`	`+// SMTIgnoreCex: yes`
`24`	`25`	`// ----`
`25`	`26`	`// Warning 9302: (212-228): Return value of low-level calls not used.`
`26`		`-// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0x0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0x0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call`
	`27`	`+// Warning 6328: (232-246): CHC: Assertion violation happens here.`