Merge pull request #13740 from ethereum/z3_4_11_2_tests

update SMTChecker tests with Z3 4.11.2

Author: Leo

.circleci/config.yml

@@ -9,20 +9,20 @@ version: 2.1
 parameters:
   ubuntu-2004-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-15
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:e4f83457bf1d6475c3189e9013da77289793a5ecd6a0e15dbec9411880b11e22"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-16
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:ee1def5806f40c35d583234e172ec5769bb9a08b6f5bbc713c1a2658846dbced"
   ubuntu-2004-clang-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-15
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:8dda4fdae312f840fbb4e25b9ef01ad3209e9014e49e4564ab0f0d2510225131"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-16
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:8f635529a10e0ddf955d6d72360261966e5fee0b5c5211070370ca2fc4e0ab7c"
   ubuntu-1604-clang-ossfuzz-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-20
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7b3ccaed3b5d37dc2cc4bbe1a1e40949266292dcdbc3ad015271ab4e5e6f5038"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-21
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:ae6b695fb8a0806702bb6a1a9616fbb33ac3288f25990fa799aab2c045c80ea1"
   emscripten-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:emscripten-13
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:f1c13f3450d1f2e53ea18ac1ac1a17e932573cb9a5ccd0fd9ef6dd44f6402fa9"
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-14
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d7d4ec28cdc3e61fc6a048b88ebdff1c5e67f3353cf1739cbaea07ec2481eb16"
   evm-version:
     type: string
     default: london

.circleci/osx_install_dependencies.sh

@@ -61,11 +61,11 @@ then
   ./scripts/install_obsolete_jsoncpp_1_7_4.sh
 
   # z3
-  z3_version="4.11.0"
+  z3_version="4.11.2"
   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" b6a4a6d587e4bfb0643db81129f0f447692fae13d4bd1bd4d93f1c0301b75ffc
+  validate_checksum "$z3_package" a56b6c40d9251a963aabe1f15731dd88ad1cb801d0e7b16e45f8b232175e165c
   unzip "$z3_package"
   rm "$z3_package"
   cp "${z3_dir}/bin/libz3.a" /usr/local/lib

CMakeLists.txt

@@ -75,7 +75,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
 
 include(EthOptions)
 configure_project(TESTS)
-set(LATEST_Z3_VERSION "4.11.0")
+set(LATEST_Z3_VERSION "4.11.2")
 set(MINIMUM_Z3_VERSION "4.8.0")
 find_package(Z3)
 if (${Z3_FOUND})

scripts/build_emscripten.sh

@@ -34,7 +34,7 @@ else
     BUILD_DIR="$1"
 fi
 
-# solbuildpackpusher/solidity-buildpack-deps:emscripten-13
+# solbuildpackpusher/solidity-buildpack-deps:emscripten-14
 # NOTE: Without `safe.directory` git would assume it's not safe to operate on /root/project since it's owned by a different user.
 # See https://github.blog/2022-04-12-git-security-vulnerability-announced/
 docker run -v "$(pwd):/root/project" -w /root/project \

scripts/error_codes.py

@@ -227,10 +227,10 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
             return False
 
     old_source_only_ids = {
-        "1584", "1823",
+        "1218", "1584", "1823",
         "1988", "2066", "2833", "3356",
         "3893", "3996", "4010", "4458", "4802",
-        "4902", "5272", "5622", "5798", "7128", "7400",
+        "4902", "5272", "5622", "5798", "5840", "7128", "7400",
         "7589", "7593", "7649", "7710",
         "8065", "8084", "8140", "8158",
         "8312", "8592", "9134", "9609",

test/cmdlineTests/model_checker_invariants_all/err

@@ -5,8 +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) || true)
+(!(x >= 1) || true)
 Reentrancy property(ies) for model_checker_invariants_all/input.sol:test:
-(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
+(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x == 0)

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) || true)
+(!(x >= 1) || true)

test/cmdlineTests/model_checker_invariants_contract_reentrancy/err

@@ -5,8 +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) || true)
+(!(x >= 1) || true)
 Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test:
-(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
+(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x == 0)

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))) || true)
+(((!(x <= 0) || !(x' >= 1)) && (!(x <= 0) || !(<errorCode> >= 1))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)

test/cmdlineTests/standard_model_checker_invariants_contract/output.json

@@ -5,12 +5,12 @@
             "component": "general",
             "errorCode": "1180",
             "formattedMessage": "Info: Contract invariant(s) for A:test:
-((x <= 0) || true)
+(!(x >= 1) || true)
 
 
 ",
             "message": "Contract invariant(s) for A:test:
-((x <= 0) || true)
+(!(x >= 1) || true)
 ",
             "severity": "info",
             "type": "Info"