Merge pull request #10845 from ethereum/smt_z3_4-8-10

Update smtCheckerTests for z3 4.8.10

Author: Leonardo

.circleci/config.yml

@@ -9,20 +9,20 @@ version: 2.1
 parameters:
   ubuntu-2004-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-4
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:aca1372dcc5edadd3db13ff1aa6807727d79e08082a48eb7cc05444c1b516ace"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-5
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:2d306b8da3485c2584a8868d656dc36c1ae50f003ff085ad2e904e312534b9b7"
   ubuntu-2004-clang-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-4
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:0954edfb48a7efa6922b4d6adf536a2fc483ca34ad62f95ec54c33a616a66974"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-5
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:4fbc7a99dd0b204fef587856d89640e4b2060d459ba15c32b89733b2a6054d7f"
   ubuntu-1604-clang-ossfuzz-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-7
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:8cbbb722b7f919264d73f61cb79cd555469f6f1d3d153b1c848a60b391faee39"
+    # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-8
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:42f47b7ddafbf57b4e48357022cf34dc38ae477b05ddc2210e7ed68d821c2019"
   emscripten-docker-image:
     type: string
-    # solbuildpackpusher/solidity-buildpack-deps:emscripten-3
-    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:e92ff672095ae31ea62ee9f4c6b552890f08c03a650d2a694609cb4385a17615"
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-4
+    default: "solbuildpackpusher/solidity-buildpack-deps@sha256:434719d8104cab47712dd1f56f255994d04eb65b802c0d382790071c1a0c074b"
 
 orbs:
   win: circleci/windows@2.2.0

.circleci/osx_install_dependencies.sh

@@ -43,13 +43,13 @@ then
   ./scripts/install_obsolete_jsoncpp_1_7_4.sh
 
   # z3
-  wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.9/z3-4.8.9-x64-osx-10.14.6.zip
-  unzip z3-4.8.9-x64-osx-10.14.6.zip
-  rm -f z3-4.8.9-x64-osx-10.14.6.zip
-  cp z3-4.8.9-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
-  cp z3-4.8.9-x64-osx-10.14.6/bin/z3 /usr/local/bin
-  cp z3-4.8.9-x64-osx-10.14.6/include/* /usr/local/include
-  rm -rf z3-4.8.9-x64-osx-10.14.6
+  wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-osx-10.15.7.zip
+  unzip z3-4.8.10-x64-osx-10.15.7.zip
+  rm -f z3-4.8.10-x64-osx-10.15.7.zip
+  cp z3-4.8.10-x64-osx-10.15.7/bin/libz3.a /usr/local/lib
+  cp z3-4.8.10-x64-osx-10.15.7/bin/z3 /usr/local/bin
+  cp z3-4.8.10-x64-osx-10.15.7/include/* /usr/local/include
+  rm -rf z3-4.8.10-x64-osx-10.15.7
 
   # evmone
   wget https://github.com/ethereum/evmone/releases/download/v0.4.0/evmone-0.4.0-darwin-x86_64.tar.gz

scripts/build_emscripten.sh

@@ -35,5 +35,6 @@ else
 fi
 
 docker run -v $(pwd):/root/project -w /root/project \
-    solbuildpackpusher/solidity-buildpack-deps@sha256:e92ff672095ae31ea62ee9f4c6b552890f08c03a650d2a694609cb4385a17615 \
+    # solbuildpackpusher/solidity-buildpack-deps:emscripten-4
+    solbuildpackpusher/solidity-buildpack-deps@sha256:434719d8104cab47712dd1f56f255994d04eb65b802c0d382790071c1a0c074b \
     ./scripts/ci/build_emscripten.sh $BUILD_DIR

test/libsolidity/smtCheckerTests/types/struct/struct_state_var.sol

@@ -12,5 +12,7 @@ contract C {
 		assert(s.a[1] == s.a[0]);
 	}
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (148-172): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 7720, a: []}\n_x = 7720\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0, a: []}\nC.f(7720)
+// Warning 6328: (148-172): CHC: Assertion violation happens here.

test/libyul/yulOptimizerTests/reasoningBasedSimplifier/addmod.yul

@@ -9,6 +9,8 @@
 
     // addmod is equal to mod of sum for small numbers
     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) {
+        // z3 <4.8.10 was able to infer that the
+        // condition below is always true.
         if eq(result, mod(add(x, y), z)) { sstore(0, 9) }
     }
 
@@ -26,6 +28,9 @@
 //     let z := calldataload(64)
 //     let result := addmod(x, y, z)
 //     if 0 { }
-//     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000)) { if 1 { sstore(0, 9) } }
+//     if and(and(lt(x, 1000), lt(y, 1000)), lt(z, 1000))
+//     {
+//         if eq(result, mod(add(x, y), z)) { sstore(0, 9) }
+//     }
 //     if and(and(gt(x, sub(0, 5)), gt(y, sub(0, 2))), eq(z, 3)) { if 0 { } }
 // }