Skip to content

Commit 4fd1cf8

Browse files
committed
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).
1 parent 0760cd7 commit 4fd1cf8

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

regression/contracts-dfcc/chain.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,4 +59,4 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
5959
rm "${name}${dfcc_suffix}-mod.c"
6060
fi
6161
$goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
62-
$cbmc "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}
62+
$cbmc --sat-solver cadical "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}

0 commit comments

Comments
 (0)