From 5dd97503a9cf5c91759df030692148026894d4b4 Mon Sep 17 00:00:00 2001
From: Lorenzo Manacorda <lorenzo@mailbox.org>
Date: Wed, 29 Mar 2023 09:26:29 +0200
Subject: [PATCH] cvc4 -> cvc5

---
 .github/scripts/install-cvc4.sh     | 33 -----------------------------
 .github/scripts/install-cvc5.sh     | 33 +++++++++++++++++++++++++++++
 .github/workflows/release.yml       |  2 +-
 src/dapp-tests/integration/tests.sh |  8 +++----
 src/dapp/README.md                  |  4 ++--
 src/dapp/libexec/dapp/dapp          |  4 ++--
 src/dapp/libexec/dapp/dapp-test     |  2 +-
 7 files changed, 43 insertions(+), 43 deletions(-)
 delete mode 100755 .github/scripts/install-cvc4.sh
 create mode 100755 .github/scripts/install-cvc5.sh

diff --git a/.github/scripts/install-cvc4.sh b/.github/scripts/install-cvc4.sh
deleted file mode 100755
index 150a727f1..000000000
--- a/.github/scripts/install-cvc4.sh
+++ /dev/null
@@ -1,33 +0,0 @@
-#!/bin/bash
-
-
-set -eux
-
-mkdir -p $HOME/.local/bin;
-
-travis_retry() {
-  cmd=$*
-  $cmd || (sleep 2 && $cmd) || (sleep 10 && $cmd)
-}
-
-fetch_cvc4_linux() {
-  VER="$1"
-  wget "https://github.com/CVC4/CVC4/releases/download/$VER/cvc4-$VER-x86_64-linux-opt"
-  chmod +x "cvc4-$VER-x86_64-linux-opt"
-  mv "cvc4-$VER-x86_64-linux-opt" "$HOME/.local/bin/cvc4"
-  echo "Downloaded cvc4 $VER"
-}
-
-fetch_cvc4_macos() {
-  VER="$1"
-  wget "https://github.com/CVC4/CVC4/releases/download/$VER/cvc4-$VER-macos-opt"
-  chmod +x "cvc4-$VER-macos-opt"
-  mv "cvc4-$VER-macos-opt" "$HOME/.local/bin/cvc4"
-  echo "Downloaded cvc4 $VER"
-}
-
-if [ "$HOST_OS" = "Linux" ]; then
-    travis_retry fetch_cvc4_linux "1.8"
-else
-    travis_retry fetch_cvc4_macos "1.8"
-fi
diff --git a/.github/scripts/install-cvc5.sh b/.github/scripts/install-cvc5.sh
new file mode 100755
index 000000000..16dca22e4
--- /dev/null
+++ b/.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
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index b5a472749..b68ff6a7e 100644
--- a/.github/workflows/release.yml
+++ b/.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 }}
 
diff --git a/src/dapp-tests/integration/tests.sh b/src/dapp-tests/integration/tests.sh
index 1b3ac5b26..ff961ef84 100755
--- a/src/dapp-tests/integration/tests.sh
+++ b/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() {
diff --git a/src/dapp/README.md b/src/dapp/README.md
index 375e7855a..e527abb02 100644
--- a/src/dapp/README.md
+++ b/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
diff --git a/src/dapp/libexec/dapp/dapp b/src/dapp/libexec/dapp/dapp
index c8021135b..2a332fe59 100755
--- a/src/dapp/libexec/dapp/dapp
+++ b/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
 
diff --git a/src/dapp/libexec/dapp/dapp-test b/src/dapp/libexec/dapp/dapp-test
index f7ddebd54..210d8e89c 100755
--- a/src/dapp/libexec/dapp/dapp-test
+++ b/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; }