From 4fd1cf85bc7dcf783a097504a5192ccdaccb9595 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 14 Aug 2024 10:50:17 +0000
Subject: [PATCH] Contracts (DFCC) regression tests: use CaDiCaL

Using CaDiCaL as SAT solver (when available) instead of MiniSat reduces
test execution time from 337 seconds down to 131 seconds (with only a
single test now taking more than 2 seconds, where its 6 seconds are
mainly spent in symex).
---
 regression/contracts-dfcc/chain.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh
index c388dc26c91..4b043e44ca7 100755
--- a/regression/contracts-dfcc/chain.sh
+++ b/regression/contracts-dfcc/chain.sh
@@ -59,4 +59,4 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
   rm "${name}${dfcc_suffix}-mod.c"
 fi
 $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
-$cbmc "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}
+$cbmc --sat-solver cadical "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}