cvc4 -> cvc5

Author: asymmetric

.github/scripts/install-cvc4.sh

@@ -0,0 +1,33 @@
+#!/bin/bash
+
+
+set -eux
+
+mkdir -p $HOME/.local/bin;
+
+travis_retry() {
+  cmd=$*
+  $cmd || (sleep 2 && $cmd) || (sleep 10 && $cmd)
+}
+
+fetch_cvc5_linux() {
+  VER="$1"
+  wget "https://github.com/cvc5/cvc5/releases/download/$VER/cvc5-$VER-x86_64-linux-opt"
+  chmod +x "cvc5-$VER-x86_64-linux-opt"
+  mv "cvc5-$VER-x86_64-linux-opt" "$HOME/.local/bin/cvc5"
+  echo "Downloaded cvc5 $VER"
+}
+
+fetch_cvc5_macos() {
+  VER="$1"
+  wget "https://github.com/cvc5/cvc5/releases/download/$VER/cvc5-$VER-macos-opt"
+  chmod +x "cvc5-$VER-macos-opt"
+  mv "cvc5-$VER-macos-opt" "$HOME/.local/bin/cvc5"
+  echo "Downloaded cvc5 $VER"
+}
+
+if [ "$HOST_OS" = "Linux" ]; then
+    travis_retry fetch_cvc5_linux "1.8"
+else
+    travis_retry fetch_cvc5_macos "1.8"
+fi

.github/scripts/install-cvc5.sh

@@ -50,7 +50,7 @@ jobs:
         run: |
           .github/scripts/install-solc.sh
           .github/scripts/install-z3.sh
-          .github/scripts/install-cvc4.sh
+          .github/scripts/install-cvc5.sh
         env:
           HOST_OS: ${{ runner.os }}
 

.github/workflows/release.yml

@@ -190,16 +190,16 @@ test_hevm_symbolic() {
 
     solc --bin-runtime -o . --overwrite "$CONTRACTS/factor.sol"
     # should find counterexample
-    hevm symbolic --code "$(<A.bin-runtime)" --sig "factor(uint x, uint y)" --smttimeout 40000 --solver cvc4 && fail || echo "hevm success: found counterexample"
+    hevm symbolic --code "$(<A.bin-runtime)" --sig "factor(uint x, uint y)" --smttimeout 40000 --solver cvc5 && fail || echo "hevm success: found counterexample"
     hevm symbolic --code "$(<"$CONTRACTS/dstoken.bin-runtime")" --sig "transferFrom(address, address, uint)" --get-models &> /dev/null || fail
 
     solc --bin-runtime -o . --overwrite "$CONTRACTS/token.sol"
-    # This one explores all paths (cvc4 is better at this)
-    hevm symbolic --code "$(<Token.bin-runtime)" --solver cvc4 || fail
+    # This one explores all paths (cvc5 is better at this)
+    hevm symbolic --code "$(<Token.bin-runtime)" --solver cvc5 || fail
 
     # The contracts A and B should be equivalent:
     solc --bin-runtime -o . --overwrite "$CONTRACTS/AB.sol"
-    hevm equivalence --code-a "$(<A.bin-runtime)" --code-b "$(<B.bin-runtime)" --solver cvc4 || fail
+    hevm equivalence --code-a "$(<A.bin-runtime)" --code-b "$(<B.bin-runtime)" --solver cvc5 || fail
 }
 
 test_custom_solc_json() {

src/dapp-tests/integration/tests.sh

@@ -16,6 +16,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 - `dapp --nix-run` invocations
 
+### Changed
+
+- Switch SMT solver from cvc4 to cvc5
+
 ## [0.35.0] - 2021-11-12
 
 ### Added

src/dapp/CHANGELOG.md

@@ -326,7 +326,7 @@ variables](../hevm/README.md#environment-variables).
 | `DAPP_TEST_DEPTH`          | `20`                       | Number of transactions to sequence per invariant cycle                                                                                             |
 | `DAPP_TEST_SMTTIMEOUT`     | `60000`                    | Timeout passed to the smt solver for symbolic tests (in ms, and per smt query)                                                                     |
 | `DAPP_TEST_MAX_ITERATIONS` | n/a                        | The number of times hevm will revisit a particular branching point when symbolically executing                                                     |
-| `DAPP_TEST_SOLVER`         | `z3`                       | Solver to use for symbolic execution (`cvc4` or `z3`)                                                                                              |
+| `DAPP_TEST_SOLVER`         | `z3`                       | Solver to use for symbolic execution (`cvc5` or `z3`)                                                                                              |
 | `DAPP_TEST_MATCH`          | n/a                        | Regex used to determine test methods to run                                                                                                        |
 | `DAPP_TEST_COV_MATCH`      | n/a                        | Regex used to determine which files to print coverage reports for. Prints all imported files by default (excluding tests and libs).                |
 | `DAPP_TEST_REPLAY`         | n/a                        | Calldata for a specific property test case to replay in the debugger                                                                               |
@@ -447,7 +447,7 @@ You can override this with the `DAPP_REMAPPINGS` environment variable.
 
     SMT options:
         --smttimeout <number>     timeout passed to the smt solver in ms (default 60000)
-        --solver <string>         name of the smt solver to use (either "z3" or "cvc4")
+        --solver <string>         name of the smt solver to use (either "z3" or "cvc5")
         --max-iterations <number> number of times we may revisit a particular branching point during symbolic execution
 
 dapp tests are written in Solidity using the `ds-test` module. To install it, run

src/dapp/README.md

@@ -31,7 +31,7 @@
 ###
 ###   SMT options:
 ### smttimeout=<number>        timeout passed to the smt solver in ms (default 60000)
-### solver=<string>            name of the smt solver to use (either 'z3' or 'cvc4')
+### solver=<string>            name of the smt solver to use (either 'z3' or 'cvc5')
 ### max-iterations=<number>    number of times we may revisit a particular branching point
 ### smtdebug                   print the SMT queries produced by hevm
 ###
@@ -80,7 +80,7 @@ rpc-block=<number>   block number (latest if not specified)
 
   SMT options:
 smttimeout=<number>        timeout passed to the smt solver in ms (default 60000)
-solver=<string>            name of the smt solver to use (either 'z3' or 'cvc4')
+solver=<string>            name of the smt solver to use (either 'z3' or 'cvc5')
 max-iterations=<number>    number of times we may revisit a particular branching point
 smtdebug                   print the SMT queries produced by hevm
 

src/dapp/libexec/dapp/dapp

@@ -18,7 +18,7 @@
 ###
 ### SMT options:
 ###   --smttimeout <number>     timeout passed to the smt solver in ms (default 600000)
-###   --solver <string>         name of the smt solver to use (either "z3" or "cvc4")
+###   --solver <string>         name of the smt solver to use (either "z3" or "cvc5")
 ###   --max-iterations <number> number of times we may revisit a particular branching point
 set -e
 have() { command -v "$1" >/dev/null; }