cvc4 -> cvc5

.github/scripts/install-cvc5.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/workflows/release.yml

@@ -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 }}
 

src/dapp-tests/integration/tests.sh

@@ -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/README.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/libexec/dapp/dapp

@@ -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-test

@@ -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; }