From 16c0838f75b9e2f31bae1dd9d4ea3238f44060a3 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Fri, 26 Aug 2022 14:33:59 +0200
Subject: [PATCH] Update docker images and tests

---
 .circleci/config.yml                          | 16 ++++++------
 .circleci/osx_install_dependencies.sh         |  4 +--
 CMakeLists.txt                                |  2 +-
 scripts/build_emscripten.sh                   |  4 +--
 .../abi/abi_encode_packed_hash.sol            |  5 ++--
 .../abi/abi_encode_with_selector_hash.sol     |  9 +++----
 .../abi/abi_encode_with_selector_vs_sig.sol   |  1 +
 .../abi/abi_encode_with_sig_hash.sol          |  4 +--
 .../abi/abi_encode_with_sig_simple.sol        |  2 +-
 .../push_as_lhs_and_rhs_bytes.sol             |  3 ++-
 .../external_calls/call_with_value_1.sol      |  2 +-
 .../external_calls/call_with_value_2.sol      |  2 +-
 .../external_call_from_constructor_3.sol      |  3 ++-
 .../external_call_this_with_value_1.sol       |  2 +-
 .../external_call_with_value_3.sol            |  4 +--
 ...nal_hash_known_code_state_reentrancy_2.sol |  4 +--
 ...h_known_code_state_reentrancy_indirect.sol |  4 ++-
 .../external_calls/external_reentrancy_1.sol  |  1 +
 .../external_calls/external_reentrancy_2.sol  |  4 +--
 .../function_selector/homer.sol               |  2 +-
 .../functions_storage_var_1_fail.sol          |  1 +
 .../imports/import_as_module_2.sol            |  8 ++++--
 .../inheritance/receive_fallback.sol          |  2 +-
 .../modifier_inside_branch_assignment.sol     |  4 ++-
 .../compound_assignment_division_3.sol        |  2 +-
 .../compound_bitwise_string_literal_3.sol     |  3 +--
 .../smtCheckerTests/out_of_bounds/array_1.sol |  3 ++-
 .../overflow/signed_guard_sub_overflow.sol    |  2 +-
 .../overflow/simple_overflow.sol              |  2 +-
 .../special/block_vars_chc_internal.sol       |  3 ++-
 .../special/tx_vars_reentrancy_1.sol          |  2 +-
 .../try_catch/try_public_var_mapping.sol      |  2 +-
 .../typecast/bytes_to_fixed_bytes_1.sol       |  8 ------
 .../typecast/bytes_to_fixed_bytes_1_fail.sol  | 25 +++++++++++++++++++
 .../typecast/string_to_bytes_push_1.sol       |  2 +-
 .../smtCheckerTests/types/array_branch_1d.sol |  4 ++-
 36 files changed, 86 insertions(+), 65 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1_fail.sol

diff --git a/.circleci/config.yml b/.circleci/config.yml
index af193b50f..f040085b2 100644
--- 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
diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh
index 37502a742..766091fdf 100755
--- 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
index d8de3d149..6680b75b2 100644
--- 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
index a678d08ab..43a402fd6 100755
--- 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
index a9608a828..1cde51069 100644
--- 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
index f60d5f52b..ae6ea018f 100644
--- 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
index b5346b049..66ec1c69b 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,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
index 61e755d82..00836f228 100644
--- 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
index 96f3e48d9..1fe781974 100644
--- 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
index 6126b5b10..cf86c7c4d 100644
--- 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
index f9293f693..813185adf 100644
--- 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
index c38658080..968095bb2 100644
--- 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
index 9d27d6d3b..ba0dc90b0 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
@@ -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
index c52e0773f..06390b12c 100644
--- 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
index fa7ef4462..2a535329a 100644
--- 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
index 37509269b..be9f698e1 100644
--- 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
index bd779b56a..ea9764e17 100644
--- 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
index 5683a5248..9cf0d3643 100644
--- 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
index 1e8ce8816..19ff2bbad 100644
--- 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
index 552a4d895..aaab88488 100644
--- 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
index a7f0c879f..e775c97a9 100644
--- 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
index 8ddef2da9..bdf2e349c 100644
--- 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
index 95ae12019..3d4c5e06a 100644
--- 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
index f8091f9df..d496baf6c 100644
--- 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
index aa90aa252..3e646ec3d 100644
--- 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
index b2d56cb12..3ac248fb2 100644
--- 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
index c26e64fcc..ee57f069d 100644
--- 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
index b28b6598c..95221c912 100644
--- 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
index e8cf49a83..d872cb669 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 = 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
index 6e4f5a620..ab355dbd2 100644
--- 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
index f1fed73c0..7d9c0ca56 100644
--- 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
index 627d06a2d..43f4b5f03 100644
--- 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
index 91166baa8..1d00e7fe3 100644
--- a/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1.sol
@@ -3,20 +3,12 @@ contract C {
 		bytes memory b = hex"00010203040506070809000102030405060708090001020304050607080900010203040506070809";
 		bytes8 c = bytes8(b);
 		assert(c == 0x0001020304050607); // should hold
-		assert(c == 0x0001020304050608); // should fail
 		bytes16 d = bytes16(b);
 		assert(d == 0x00010203040506070809000102030405);
-		assert(d == 0x00010203040506070809000102030406); // should fail
 		bytes24 e = bytes24(b);
 		assert(e == 0x000102030405060708090001020304050607080900010203); // should hold
-		assert(e == 0x000102030405060708090001020304050607080900010204); // should fail
 		bytes32 g = bytes32(b);
 		assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold
-		assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail
 	}
 }
 // ----
-// Warning 6328: (225-256): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x0\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
-// Warning 6328: (352-399): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
-// Warning 6328: (526-589): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x0\n\nTransaction trace:\nC.constructor()\nC.f()
-// Warning 6328: (732-811): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0x01020304050607\nd = 0x010203040506070809000102030405\ne = 0x0102030405060708090001020304050607080900010203\ng = 0x01020304050607080900010203040506070809000102030405060708090001\n\nTransaction trace:\nC.constructor()\nC.f()
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
new file mode 100644
index 000000000..40cd27776
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/bytes_to_fixed_bytes_1_fail.sol
@@ -0,0 +1,25 @@
+contract C {
+	function f() external pure {
+		bytes memory b = hex"00010203040506070809000102030405060708090001020304050607080900010203040506070809";
+		bytes8 c = bytes8(b);
+		//assert(c == 0x0001020304050607); // should hold
+		assert(c == 0x0001020304050608); // should fail
+		bytes16 d = bytes16(b);
+		//assert(d == 0x00010203040506070809000102030405);
+		assert(d == 0x00010203040506070809000102030406); // should fail
+		bytes24 e = bytes24(b);
+		//assert(e == 0x000102030405060708090001020304050607080900010203); // should hold
+		assert(e == 0x000102030405060708090001020304050607080900010204); // should fail
+		bytes32 g = bytes32(b);
+		//assert(g == 0x0001020304050607080900010203040506070809000102030405060708090001); // should hold
+		assert(g == 0x0001020304050607080900010203040506070809000102030405060708090002); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (227-258): CHC: Assertion violation happens here.
+// Warning 6328: (356-403): CHC: Assertion violation happens here.
+// Warning 6328: (532-595): CHC: Assertion violation happens here.
+// Warning 6328: (740-819): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol
index 4910c417e..33546b49c 100644
--- a/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol
+++ b/test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol
@@ -11,4 +11,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\nx = [0x61, 0x62, 0x63, 0x61]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()
+// Warning 6328: (132-160): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()
diff --git a/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol b/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
index b04c632e9..b6f19302b 100644
--- a/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
+++ b/test/libsolidity/smtCheckerTests/types/array_branch_1d.sol
@@ -12,4 +12,6 @@ contract C
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 6328: (143-159): CHC: Assertion violation happens here.
+// Warning 1218: (143-159): CHC: Error trying to invoke SMT solver.
+// Warning 6328: (143-159): CHC: Assertion violation might happen here.
+// Warning 4661: (143-159): BMC: Assertion violation happens here.