Merge pull request #12974 from ethereum/smt_tests_z3_16

Leo · web-flow · commit 84c64edfeea3 · 2022-05-04T21:24:15.000+02:00
update smt tests z3 4.8.16
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-11
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:9928dc357829e475e8729c62a1c2d495dbb41cb9fe4c4b115a5568be8e1ed69e"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-12
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:5087cc068b48787e89887804e632120b3e65bc5c25086bdf7b152be4fe5fc9ba"
   ubuntu-2004-clang-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-11
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:72fb9574c90e8ef908dce4c9dd9788ff4de708b504d970cd9146eed8911c313e"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-12
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7f53f1bc3d89bdfb0725f604efbbec570d80ffa9b731b47a4842f4e286de0355"
   ubuntu-1604-clang-ossfuzz-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-16
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:fe54d8e5409827d43edb0dc8ad0d9e4232a675050ceb271c873b73e5ee267938"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-17
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:85b298c763adf5c516238246beb283640eb555e79e7ad6a8e7a6c9ed47ef6324"
   emscripten-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:emscripten-9
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24"
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-10
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:bd23831e0025e35a106005b4ac06cb3618f690bfa2833a5881b573c02d35d9fc"
   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.14"
+  z3_version="4.8.16"
   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" 1341671670e0c4e72da80815128a68975ee90816d50ceaf6bd820f06babe2cfd
+  validate_checksum "$z3_package" 71ed7b6d10c01198187df72cccb8eb6de6d9aa2bf9557b3dd052032524b598a5
   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.14")
+set(LATEST_Z3_VERSION "4.8.16")
 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-9
+# solbuildpackpusher/solidity-buildpack-deps:emscripten-10
 docker run -v "$(pwd):/root/project" -w /root/project \
-    solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24\
+    solbuildpackpusher/solidity-buildpack-deps@sha256:bd23831e0025e35a106005b4ac06cb3618f690bfa2833a5881b573c02d35d9fc\
     ./scripts/ci/build_emscripten.sh "$BUILD_DIR"
diff --git a/test/cmdlineTests/model_checker_invariants_all/err b/test/cmdlineTests/model_checker_invariants_all/err
@@ -5,10 +5,8 @@ Warning: Return value of low-level calls not used.
   | 		^^^^^^^^^^^
 
 Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test:
-(x <= 0)
+((x <= 0) || true)
 Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
-((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
-<errorCode> = 1 -> Assertion failed at assert(x < 10)
-<errorCode> = 3 -> Assertion failed at assert(x < 10)
+<errorCode> = 1 -> Assertion failed at assert(x == 0)
diff --git a/test/cmdlineTests/model_checker_invariants_all/input.sol b/test/cmdlineTests/model_checker_invariants_all/input.sol
@@ -4,9 +4,6 @@ contract test {
 	uint x;
     function f(address _a) public {
 		_a.call("");
-		assert(x < 10);
+		assert(x == 0);
     }
-	function g() public view {
-		assert(x < 10);
-	}
 }
diff --git a/test/cmdlineTests/model_checker_invariants_contract/err b/test/cmdlineTests/model_checker_invariants_contract/err
@@ -1,2 +1,2 @@
 Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test:
-(x <= 0)
+((x <= 0) || true)
diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
@@ -5,10 +5,8 @@ Warning: Return value of low-level calls not used.
   | 		^^^^^^^^^^^
 
 Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test:
-(x <= 0)
+((x <= 0) || true)
 Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
-((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
-<errorCode> = 1 -> Assertion failed at assert(x < 10)
-<errorCode> = 3 -> Assertion failed at assert(x < 10)
+<errorCode> = 1 -> Assertion failed at assert(x == 0)
diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol
@@ -4,9 +4,6 @@ contract test {
 	uint x;
     function f(address _a) public {
 		_a.call("");
-		assert(x < 10);
+		assert(x == 0);
     }
-	function g() public view {
-		assert(x < 10);
-	}
 }
diff --git a/test/cmdlineTests/model_checker_invariants_reentrancy/err b/test/cmdlineTests/model_checker_invariants_reentrancy/err
@@ -5,6 +5,6 @@ Warning: Return value of low-level calls not used.
   | 		^^^^^^^^^^^
 
 Info: Reentrancy property(ies) for model_checker_invariants_reentrancy/input.sol:test:
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)
diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract/output.json
@@ -1,7 +1,7 @@
 {"errors":[{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
-(x <= 0)
+((x <= 0) || true)
 
 
 ","message":"Contract invariant(s) for A:test:
-(x <= 0)
+((x <= 0) || true)
 ","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/input.json
@@ -8,10 +8,7 @@
 					uint x;
 					function f(address _a) public {
 						_a.call(\"\");
-						assert(x < 10);
-					}
-					function g() public view {
-						assert(x < 10);
+						assert(x == 10);
 					}
 				}"
 		}
diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json
@@ -4,22 +4,28 @@
 7 | \t\t\t\t\t\t_a.call(\"\");
   | \t\t\t\t\t\t^^^^^^^^^^^
 
-","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
-(x <= 0)
-Reentrancy property(ies) for A:test:
-((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
-<errorCode> = 0 -> no errors
-<errorCode> = 1 -> Assertion failed at assert(x < 10)
-<errorCode> = 3 -> Assertion failed at assert(x < 10)
+","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+Counterexample:
+x = 0
+_a = 0x0
 
+Transaction trace:
+test.constructor()
+State: x = 0
+test.f(0x0)
+    _a.call(\"\") -- untrusted external call
+ --> A:8:7:
+  |
+8 | \t\t\t\t\t\tassert(x == 10);
+  | \t\t\t\t\t\t^^^^^^^^^^^^^^^
+
+","message":"CHC: Assertion violation happens here.
+Counterexample:
+x = 0
+_a = 0x0
 
-","message":"Contract invariant(s) for A:test:
-(x <= 0)
-Reentrancy property(ies) for A:test:
-((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
-<errorCode> = 0 -> no errors
-<errorCode> = 1 -> Assertion failed at assert(x < 10)
-<errorCode> = 3 -> Assertion failed at assert(x < 10)
-","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
+Transaction trace:
+test.constructor()
+State: x = 0
+test.f(0x0)
+    _a.call(\"\") -- untrusted external call","severity":"warning","sourceLocation":{"end":166,"file":"A","start":151},"type":"Warning"}],"sources":{"A":{"id":0}}}
diff --git a/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json
@@ -5,13 +5,13 @@
   | \t\t\t\t\t\t^^^^^^^^^^^
 
 ","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Reentrancy property(ies) for A:test:
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)
 
 
 ","message":"Reentrancy property(ies) for A:test:
-((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
+(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)
 ","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp
@@ -69,7 +69,17 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E
 	else
 		BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice."));
 
-	auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "no");
+	static auto removeInv = [](vector<SyntaxTestError>&& errors) {
+		vector<SyntaxTestError> filtered;
+		for (auto&& e: errors)
+			if (e.errorId != 1180_error)
+				filtered.emplace_back(e);
+		return filtered;
+	};
+	if (m_modelCheckerSettings.invariants.invariants.empty())
+		m_expectations = removeInv(move(m_expectations));
+
+	auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "yes");
 	if (ignoreInv == "no")
 		m_modelCheckerSettings.invariants = ModelCheckerInvariants::All();
 	else if (ignoreInv == "yes")
diff --git a/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol b/test/libsolidity/smtCheckerTests/abi/abi_encode_with_selector_hash.sol
@@ -3,7 +3,8 @@ contract C {
 		require(a == b);
 		bytes memory b1 = abi.encodeWithSelector(sel, a, a, a, a);
 		bytes memory b2 = abi.encodeWithSelector(sel, b, a, b, a);
-		assert(keccak256(b1) == keccak256(b2));
+		// Disabled because of OSX nondeterminism
+		//assert(keccak256(b1) == keccak256(b2));
 
 		bytes memory b3 = abi.encodeWithSelector(0xcafecafe, a, a, a, a);
 		assert(keccak256(b1) == keccak256(b3)); // should fail
@@ -13,9 +14,10 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (333-371): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (390-428): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (333-371): CHC: Assertion violation might happen here.
-// Warning 6328: (390-428): CHC: Assertion violation might happen here.
-// Warning 4661: (333-371): BMC: Assertion violation happens here.
-// Warning 4661: (390-428): BMC: Assertion violation happens here.
+// 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.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
@@ -19,4 +19,4 @@ contract C {
 // SMTEngine: all
 // SMTIgnoreOS: macos
 // ----
-// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g()
+// Warning 6328: (199-229): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol
@@ -18,5 +18,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (265-310): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes_2d.sol
@@ -22,5 +22,6 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
 // Warning 6328: (435-508): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
@@ -16,8 +16,7 @@ contract C {
 // Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (212-218): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ msg.value: 11 }\nState: c = 1\nC.inv()
-// Info 1180: Contract invariant(s) for :C:\n(((11 * c) + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n
+// Warning 6328: (180-219): CHC: Assertion violation happens here.
 // Warning 2661: (82-85): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (154-160): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (212-218): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
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.
+// 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: (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/crypto/crypto_functions_same_input_over_state_same_output_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
@@ -48,12 +48,10 @@ contract C {
 // Warning 1218: (693-712): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (716-735): CHC: Error trying to invoke SMT solver.
 // Warning 1218: (739-758): CHC: Error trying to invoke SMT solver.
-// Warning 1218: (762-781): CHC: Error trying to invoke SMT solver.
 // Warning 6328: (693-712): CHC: Assertion violation might happen here.
 // Warning 6328: (716-735): CHC: Assertion violation might happen here.
 // Warning 6328: (739-758): CHC: Assertion violation might happen here.
-// Warning 6328: (762-781): CHC: Assertion violation might happen here.
+// Warning 6328: (762-781): CHC: Assertion violation happens here.
 // Warning 4661: (693-712): BMC: Assertion violation happens here.
 // Warning 4661: (716-735): BMC: Assertion violation happens here.
 // Warning 4661: (739-758): BMC: Assertion violation happens here.
-// Warning 4661: (762-781): BMC: 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.
+// 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 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
@@ -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/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,4 +42,6 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 2018: (33-88): Function state mutability can be restricted to view
-// Warning 6328: (367-381): CHC: Assertion violation happens here.
+// 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.
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,7 +44,5 @@ 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 might happen here.
-// Warning 4661: (437-463): BMC: Assertion violation happens here.
+// Warning 6328: (437-463): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol b/test/libsolidity/smtCheckerTests/functions/getters/array_1.sol
@@ -14,6 +14,7 @@ contract C {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (187-201): CHC: Assertion violation happens here.\nCounterexample:\na = [0, 0, 0, 0]\ny = 0\n\nTransaction trace:\nC.constructor()\nState: a = [0, 0, 0, 0]\nC.f()
+// Warning 6328: (187-201): CHC: Assertion violation happens here.
 // Info 1180: Contract invariant(s) for :C:\n!(a.length <= 2)\n
diff --git a/test/libsolidity/smtCheckerTests/functions/payable_2.sol b/test/libsolidity/smtCheckerTests/functions/payable_2.sol
@@ -24,4 +24,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 35 }\n    C.i() -- internal call
+// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 1 }\n    C.i() -- internal call
diff --git a/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol
@@ -27,7 +27,5 @@ contract C
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (290-305): CHC: Error trying to invoke SMT solver.
-// Warning 6328: (290-305): CHC: Assertion violation might happen here.
+// Warning 6328: (290-305): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 15\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false)
 // Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, true, false)
-// Warning 4661: (290-305): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
@@ -19,4 +19,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Info 1180: Contract invariant(s) for :C:\n!(s.x.length <= 2)\n
+// Warning 6368: (196-202): CHC: Out of bounds access might happen here.
diff --git a/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol b/test/libsolidity/smtCheckerTests/overflow/unsigned_mul_overflow.sol
@@ -5,5 +5,6 @@ contract C  {
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// 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.
diff --git a/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol
@@ -32,4 +32,4 @@ contract C {
 // ====
 // SMTEngine: chc
 // ----
-// 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
+// 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
diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_nested_2.sol
diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol
diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol
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
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
diff --git a/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol b/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol
diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion.sol
diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol
diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol
diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol
diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol

Original file line number	Diff line number	Diff line change
`@@ -4,9 +4,6 @@ contract test {`
`4`	`4`	`uint x;`
`5`	`5`	`function f(address _a) public {`
`6`	`6`	`_a.call("");`
`7`		`- assert(x < 10);`
	`7`	`+ assert(x == 0);`
`8`	`8`	`}`
`9`		`- function g() public view {`
`10`		`- assert(x < 10);`
`11`		`- }`
`12`	`9`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,2 +1,2 @@`
`1`	`1`	`Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test:`
`2`		`-(x <= 0)`
	`2`	`+((x <= 0) \|\| true)`