Merge pull request #13439 from ethereum/z3_4_8_11_smt_tests

Leo · web-flow · commit e048ba4d7579 · 2022-08-30T12:51:13.000+02:00
Update SMT tests with z3 4.11.0
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-13
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:aa64242ecba4f040a839eadfaf20e8489cf93d1cb96ab90df2b240cdbbfe7f7c"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-14
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d1ef23849db4c5462b248d89c111da4009b153cbd5002cb8755b0580312be581"
   ubuntu-2004-clang-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-13
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:caaf8d42aaf07397d1540e570f096a4fb1ef11fda7da3f1141d8852ec8322a9e"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-14
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:beb8c91998ec0df99a488900b3723a06f1122f0954fc73786b6c53fd73a6408d"
   ubuntu-1604-clang-ossfuzz-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-18
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:048002d71a1f86f83dedb79dd057760b752256c75646ba5ad5c1bbe92e1695aa"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-19
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:8c9bf1813c261d781f4c65fceed2dfb3ecf5be9ecf49bddbd250b570a7f3baea"
   emscripten-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:emscripten-12
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:65a82268792a5a2ee85ad432baf04a056c3a4006941ab3a4416eb1a0614883f3"
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-13
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:f1c13f3450d1f2e53ea18ac1ac1a17e932573cb9a5ccd0fd9ef6dd44f6402fa9"
   evm-version:
     type: string
     default: london
@@ -1087,6 +1087,9 @@ jobs:
     environment:
       EVM: << pipeline.parameters.evm-version >>
       OPTIMIZE: 0
+      # The high parallelism in this job is causing the SMT tests to run out of memory,
+      # so disabling for now.
+      SOLTEST_FLAGS: --no-smt
     <<: *steps_soltest
 
   t_ubu_release_soltest_all: &t_ubu_release_soltest_all
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.17"
+  z3_version="4.11.0"
   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" 189667930517aee07f1ce36485d5924a9a2cb4f8c3c9586b03e714a2c657541a
+  validate_checksum "$z3_package" b6a4a6d587e4bfb0643db81129f0f447692fae13d4bd1bd4d93f1c0301b75ffc
   unzip "$z3_package"
   rm "$z3_package"
   cp "${z3_dir}/bin/libz3.a" /usr/local/lib
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -69,7 +69,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
 
 include(EthOptions)
 configure_project(TESTS)
-set(LATEST_Z3_VERSION "4.8.17")
+set(LATEST_Z3_VERSION "4.11.0")
 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-12
+# solbuildpackpusher/solidity-buildpack-deps:emscripten-13
 docker run -v "$(pwd):/root/project" -w /root/project \
-    solbuildpackpusher/solidity-buildpack-deps@sha256:65a82268792a5a2ee85ad432baf04a056c3a4006941ab3a4416eb1a0614883f3 \
+    solbuildpackpusher/solidity-buildpack-deps@sha256:f1c13f3450d1f2e53ea18ac1ac1a17e932573cb9a5ccd0fd9ef6dd44f6402fa9 \
     ./scripts/ci/build_emscripten.sh "$BUILD_DIR"
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_packed_hash.sol
@@ -11,7 +11,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
-// Warning 1218: (281-319): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (281-319): CHC: Assertion violation might happen here.
-// Warning 4661: (281-319): BMC: Assertion violation happens here.
+// Warning 6328: (281-319): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 0\n\nTransaction trace:\nC.constructor()\nC.abiencodePackedHash(0, 0)
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
@@ -13,11 +13,8 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 2072: (161-176): Unused local variable.
-// Warning 1218: (379-417): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (436-474): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (379-417): CHC: Assertion violation might happen here.
-// Warning 6328: (436-474): CHC: Assertion violation might happen here.
-// Warning 4661: (379-417): BMC: Assertion violation happens here.
-// Warning 4661: (436-474): BMC: Assertion violation happens here.
+// Warning 6328: (379-417): CHC: Assertion violation happens here.
+// Warning 6328: (436-474): CHC: 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
@@ -9,5 +9,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
+// Warning 1218: (294-324): CHC: Error trying to invoke SMT solver.
 // 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/abi/abi_encode_with_sig_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_hash.sol
@@ -13,7 +13,5 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (394-432): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (337-375): CHC: Assertion violation happens here.
-// Warning 6328: (394-432): CHC: Assertion violation might happen here.
-// Warning 4661: (394-432): BMC: Assertion violation happens here.
+// Warning 6328: (394-432): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_sig_simple.sol
@@ -25,7 +25,7 @@ contract C {
 // ----
 // Warning 5667: (107-122): Unused function parameter. Remove or comment out the variable name to silence this warning.
 // Warning 1218: (824-854): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (543-573): CHC: Assertion violation happens here.
+// Warning 6328: (543-573): CHC: Assertion violation happens here.\nCounterexample:\n\nt = false\nx = 0\ny = 0\nz = 0\nb5 = []\nb6 = []\n\nTransaction trace:\nC.constructor()\nC.abiEncodeSimple(sig, false, 0, 0, 0, a, b)
 // Warning 6328: (664-694): CHC: Assertion violation happens here.
 // Warning 6328: (713-743): CHC: Assertion violation happens here.
 // Warning 6328: (824-854): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_and_rhs_bytes.sol
@@ -12,5 +12,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (203-244): CHC: Assertion violation happens here.
+// Warning 6328: (203-244): CHC: Assertion violation happens here.\nCounterexample:\nb = [0x0, 0x0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()
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/call_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol
@@ -11,5 +11,5 @@ contract C {
 // ----
 // Warning 9302: (96-116): Return value of low-level calls not used.
 // Warning 6328: (120-156): CHC: Assertion violation might happen here.
-// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n    i.call{value: 0}("") -- untrusted external call
+// Warning 6328: (175-210): CHC: Assertion violation happens here.
 // Warning 4661: (120-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
@@ -18,6 +18,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // 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_this_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol
@@ -11,4 +11,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (157-192): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.h() -- trusted external call
+// Warning 6328: (157-192): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol
@@ -14,8 +14,6 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 1218: (202-236): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (150-183): CHC: Assertion violation might happen here.
-// Warning 6328: (202-236): CHC: Assertion violation might happen here.
+// Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    i.f{value: 20}() -- untrusted external call
 // Warning 4661: (150-183): BMC: Assertion violation happens here.
-// Warning 4661: (202-236): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol
@@ -42,6 +42,4 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 2018: (33-88): Function state mutability can be restricted to view
-// Warning 1218: (367-381): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (367-381): CHC: Assertion violation might happen here.
-// Warning 4661: (367-381): BMC: Assertion violation happens here.
+// Warning 6328: (367-381): CHC: Assertion violation happens here.
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
@@ -44,5 +44,7 @@ contract C {
 // 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_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_1.sol
@@ -15,6 +15,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 1218: (206-220): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (206-220): CHC: Assertion violation might happen here.
diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_reentrancy_2.sol
@@ -13,6 +13,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// 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.
+// 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/function_selector/homer.sol b/test/libsolidity/smtCheckerTests/function_selector/homer.sol
@@ -43,4 +43,4 @@ contract Homer is ERC165, Simpson {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (1340-1395): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.check()\n    Homer.supportsInterface(0x73b6b492) -- internal call\n    Homer.supportsInterface(0x01ffc9a7) -- internal call\n    Homer.supportsInterface(0x8b9eb9ca) -- internal call
+// Warning 6328: (1340-1395): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nHomer.constructor()\nHomer.supportsInterface(0x01ffc9a7)\nHomer.check()\n    Homer.supportsInterface(0x73b6b492) -- internal call\n    Homer.supportsInterface(0x01ffc9a7) -- internal call\n    Homer.supportsInterface(0x8b9eb9ca) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol
@@ -13,5 +13,6 @@ contract C
 
 // ====
 // SMTEngine: all
+// SMTIgnoreOS: macos
 // ----
 // Warning 6328: (112-125): CHC: Assertion violation happens here.\nCounterexample:\na = 0\n\nTransaction trace:\nC.constructor()\nState: a = 0\nC.g()\n    C.f(0) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol
@@ -18,5 +18,9 @@ function f(uint _x) pure {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n    s1.sol:f(200) -- internal call\n    s1.sol:f(0) -- internal call\n    A:f(10) -- internal call\n    A:f(0) -- internal call
-// Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n    s1.sol:f(200) -- internal call\n    s1.sol:f(0) -- internal call
+// Warning 1218: (A:50-64): CHC: Error trying to invoke SMT solver.
+// Warning 1218: (s1.sol:28-44): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (A:50-64): CHC: Assertion violation might happen here.
+// Warning 6328: (s1.sol:28-44): CHC: Assertion violation might happen here.
+// Warning 4661: (s1.sol:28-44): BMC: Assertion violation happens here.
+// Warning 4661: (A:50-64): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol b/test/libsolidity/smtCheckerTests/inheritance/receive_fallback.sol
@@ -21,6 +21,6 @@ contract B is A {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ msg.value: 2 }
+// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.receive(){ msg.value: 1 }
 // Warning 6328: (136-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()
 // Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 0\n\nTransaction trace:\nB.constructor()\nState: y = 0, x = 0\nB.fallback()
diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_inside_branch_assignment.sol
@@ -20,4 +20,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (254-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, owner = 0x0\ny = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, owner = 0x0\nC.g(1)\n    C.f() -- internal call
+// Warning 1218: (254-267): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (254-267): CHC: Assertion violation might happen here.
+// Warning 4661: (254-267): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_assignment_division_3.sol
@@ -12,4 +12,4 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (162-181): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\np = 0\n\nTransaction trace:\nC.constructor()\nC.f(2, 0)
+// Warning 6328: (162-181): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_string_literal_3.sol
@@ -18,5 +18,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (229-276): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x6062606464666060606260646466606060626064646660606062606464666060\nz = 0x6062606464666060606260646466606060626064646660606062606464666060\n\nTransaction trace:\nC.constructor()\nC.f()
-// Warning 6328: (394-437): CHC: Assertion violation might happen here.
-// Warning 4661: (394-437): BMC: Assertion violation happens here.
+// Warning 6328: (394-437): CHC: Assertion violation happens here.\nCounterexample:\n\ny = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\nz = 0x63666566676e616263666566676e616263666566676e616263666566676e6162\n\nTransaction trace:\nC.constructor()\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol b/test/libsolidity/smtCheckerTests/out_of_bounds/array_1.sol
@@ -21,6 +21,7 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 3944: (181-184): CHC: Underflow (resulting value less than 0) might happen here.
 // Warning 6368: (259-263): CHC: Out of bounds access happens here.\nCounterexample:\na = [0], l = 1\n = 0\n\nTransaction trace:\nC.constructor()\nState: a = [], l = 0\nC.p()\nState: a = [0], l = 1\nC.r()
-// Info 1180: Contract invariant(s) for :C:\n((a.length + ((- 1) * l)) <= 0)\n
 // Warning 2661: (112-115): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4144: (181-184): BMC: Underflow (resulting value less than 0) happens here.
diff --git a/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/signed_guard_sub_overflow.sol
@@ -8,4 +8,4 @@ contract C  {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 0\ny = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, (- 57896044618658097711785492504343953926634992332820282019728792003956564819968))
+// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = 57896044618658097711785492504343953926634992332820282019728792003956564819967\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(57896044618658097711785492504343953926634992332820282019728792003956564819967, (- 1))
diff --git 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 = 1\nb = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 115792089237316195423570985008687907853269984665640564039457584007913129639935)
+// 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)
diff --git a/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol
@@ -31,5 +31,6 @@ contract C {
 }
 // ====
 // SMTEngine: chc
+// SMTIgnoreOS: macos
 // ----
-// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x1e28, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x1e28, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n    C.g() -- internal call
+// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n    C.g() -- internal call
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 = 9726\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2070 }\n    _i.f() -- untrusted external call, synthesized as:\n        C.g(0){ msg.value: 0 } -- reentrant call\n            _i.f() -- untrusted external call
+// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 868\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 500 }\n    _i.f() -- untrusted external call, synthesized as:\n        C.g(0){ msg.value: 0 } -- reentrant call\n            _i.f() -- untrusted external call
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,4 +21,4 @@ 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()
diff --git a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol
diff --git a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1_fail.sol b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1_fail.sol
diff --git a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol
diff --git a/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol b/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol

Original file line number	Diff line number	Diff line change
`@@ -12,5 +12,6 @@ contract C {`
`12`	`12`	`}`
`13`	`13`	`// ====`
`14`	`14`	`// SMTEngine: all`
	`15`	`+// SMTIgnoreOS: macos`
`15`	`16`	`// ----`
`16`		`-// Warning 6328: (203-244): CHC: Assertion violation happens here.`
	`17`	`+// Warning 6328: (203-244): CHC: Assertion violation happens here.\nCounterexample:\nb = [0x0, 0x0]\nlength = 2\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.f()`