Support bitwuzla, cvc5, z3 as solver attribute values

docs/src/build-from-source.md

@@ -13,6 +13,8 @@ In general, the following dependencies are required to build Kani from source.
 1. Cargo installed via [rustup](https://rustup.rs/)
 2. [CBMC](https://github.com/diffblue/cbmc) (latest release)
 3. [Kissat](https://github.com/arminbiere/kissat) (Release 4.0.1)
+3. [Z3](https://github.com/Z3Prover/z3)
+4. [cvc5](https://github.com/cvc5/cvc5)
 
 Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms.
 

docs/src/reference/attributes.md

@@ -206,6 +206,9 @@ At present, `<solver>` can be one of:
  - `minisat`: [MiniSat](http://minisat.se/).
  - `cadical` (default): [CaDiCaL](https://github.com/arminbiere/cadical).
  - `kissat`: [kissat](https://github.com/arminbiere/kissat).
+ - `z3`: [Z3](https://github.com/Z3Prover/z3/).
+ - `bitwuzla`: [Bitwuzla](https://github.com/bitwuzla/bitwuzla).
+ - `cvc5`: [cvc5](https://github.com/cvc5/cvc5).
  - `bin="<SAT_SOLVER_BINARY>"`: A custom solver binary, `"<SAT_SOLVER_BINARY>"`, that must be in path.
 
 ### Example

kani-driver/src/call_cbmc.rs

@@ -279,10 +279,16 @@ impl KaniSession {
         };
 
         match solver {
+            CbmcSolver::Bitwuzla => {
+                args.push("--bitwuzla".into());
+            }
             CbmcSolver::Cadical => {
                 args.push("--sat-solver".into());
                 args.push("cadical".into());
             }
+            CbmcSolver::Cvc5 => {
+                args.push("--cvc5".into());
+            }
             CbmcSolver::Kissat => {
                 args.push("--external-sat-solver".into());
                 args.push("kissat".into());
@@ -291,6 +297,9 @@ impl KaniSession {
                 // Minisat is currently CBMC's default solver, so no need to
                 // pass any arguments
             }
+            CbmcSolver::Z3 => {
+                args.push("--z3".into());
+            }
             CbmcSolver::Binary(solver_binary) => {
                 // Check if the specified binary exists in path
                 if which::which(solver_binary).is_err() {

kani_metadata/src/cbmc_solver.rs

@@ -10,15 +10,24 @@ use strum_macros::{AsRefStr, EnumString, VariantNames};
 #[derive(Debug, Clone, AsRefStr, EnumString, VariantNames, PartialEq, Eq, Serialize, Deserialize)]
 #[strum(serialize_all = "snake_case")]
 pub enum CbmcSolver {
+    /// Bitwuzla SMT solver
+    Bitwuzla,
+
     /// CaDiCaL which is available in CBMC as of version 5.77.0
     Cadical,
 
+    /// cvc5 SMT solver
+    Cvc5,
+
     /// The kissat solver that is included in the Kani bundle
     Kissat,
 
     /// MiniSAT (CBMC's default solver)
     Minisat,
 
+    /// Z3 SMT solver
+    Z3,
+
     /// A solver binary variant whose argument gets passed to
     /// `--external-sat-solver`. The specified binary must exist in path.
     #[strum(disabled, serialize = "bin=<SAT_SOLVER_BINARY>")]

scripts/setup/macos/install_deps.sh

@@ -14,6 +14,14 @@ brew update
 brew install python@3 || true
 brew link --overwrite python@3
 
+# Install SMT solvers being used in regression tests
+brew install z3
+ARCH=$(uname -m)
+curl -L --remote-name https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.0/cvc5-macOS-${ARCH}-static.zip
+sudo unzip -o -j -d /usr/local/bin cvc5-macOS-${ARCH}-static.zip cvc5-macOS-${ARCH}-static/bin/cvc5
+rm cvc5-macOS-${ARCH}-static.zip
+cvc5 --version
+
 # Get the directory containing this script
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 

scripts/setup/ubuntu/install_deps.sh

@@ -16,6 +16,7 @@ DEPS=(
   gpg-agent
   make
   patch
+  z3
   zlib1g
   zlib1g-dev
 )
@@ -30,6 +31,12 @@ sudo apt-get --yes update
 
 sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${DEPS[@]}"
 
+ARCH=$(uname -m)
+curl -L --remote-name https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.0/cvc5-Linux-${ARCH}-static.zip
+sudo unzip -o -j -d /usr/local/bin cvc5-Linux-${ARCH}-static.zip cvc5-Linux-${ARCH}-static/bin/cvc5
+rm cvc5-Linux-${ARCH}-static.zip
+cvc5 --version
+
 # Get the directory containing this script
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 

tests/expected/function-contract/as-assertions/assert-postconditions.rs

@@ -23,6 +23,7 @@ fn add_one(add_one_ptr: &mut u32) {
 }
 
 #[kani::proof_for_contract(add_three)]
+#[kani::solver(z3)]
 fn prove_add_three() {
     let mut i = kani::any();
     add_three(&mut i);

tests/expected/loop-contract/loop_assigns_for_vec.rs

@@ -12,6 +12,7 @@ use std::ptr;
 use std::ptr::slice_from_raw_parts;
 
 #[kani::proof]
+#[kani::solver(z3)]
 fn main() {
     let mut i = 0;
     let a: [u8; 3] = kani::any();

tests/kani/Quantifiers/arbitrary_range.rs

@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
+
+// See https://github.com/model-checking/kani/issues/4226
+
+#[kani::proof]
+#[kani::solver(cvc5)]
+fn main() {
+    const N: usize = 100;
+    let a: [i32; N] = kani::any();
+    let i = kani::any();
+    kani::assume(i < N - 1);
+    kani::assume(kani::forall!(|j in (1, i)| a[j] < 10));
+    kani::assume(a[i] < 10);
+    assert!(kani::forall!(|j in (1, i+1)| a[j] < 10));
+}
+
+#[kani::proof]
+fn bounded() {
+    const N: usize = 100;
+    let a: [i32; N] = kani::any();
+    let i = 20;
+    kani::assume(i < N - 1);
+    kani::assume(kani::forall!(|j in (1, i)| a[j] < 10));
+    kani::assume(a[i] < 10);
+    assert!(kani::forall!(|j in (1, i+1)| a[j] < 10));
+}