Add cadical to the list of available solvers (rust-lang#2217)

Author: zhassan-aws

kani-driver/src/call_cbmc.rs

@@ -205,6 +205,10 @@ impl KaniSession {
         };
 
         match solver {
+            CbmcSolver::Cadical => {
+                args.push("--sat-solver".into());
+                args.push("cadical".into());
+            }
             CbmcSolver::Kissat => {
                 args.push("--external-sat-solver".into());
                 args.push("kissat".into());

kani_metadata/src/cbmc_solver.rs

@@ -20,6 +20,9 @@ use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 )]
 #[strum(serialize_all = "snake_case")]
 pub enum CbmcSolver {
+    /// CaDiCaL which is available in CBMC as of version 5.77.0
+    Cadical,
+
     /// The kissat solver that is included in the Kani bundle
     Kissat,
 

tests/ui/solver-attribute/cadical/expected

@@ -0,0 +1,2 @@
+Solving with CaDiCaL
+VERIFICATION:- SUCCESSFUL

tests/ui/solver-attribute/cadical/test.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `cadical` is a valid argument to `kani::solver`
+
+#[kani::proof]
+#[kani::solver(cadical)]
+fn check() {
+    let mut a = [2, 3, 1];
+    a.sort();
+    assert_eq!(a[0], 1);
+    assert_eq!(a[1], 2);
+    assert_eq!(a[2], 3);
+}

tests/ui/solver-option/cadical/expected

@@ -0,0 +1,2 @@
+Solving with CaDiCaL
+VERIFICATION:- SUCCESSFUL

tests/ui/solver-option/cadical/test.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --solver cadical
+
+//! Checks that the `cadical` is supported as an argument to `--solver`
+
+#[kani::proof]
+fn check_solver_option() {
+    let v = vec![kani::any(), 2];
+    let v_copy = v.clone();
+    assert_eq!(v, v_copy);
+}