Skip to content

Commit

Permalink
Contracts (DFCC) regression tests: use CaDiCaL
Browse files Browse the repository at this point in the history
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).
  • Loading branch information
tautschnig committed Aug 14, 2024
1 parent 0760cd7 commit 4fd1cf8
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion regression/contracts-dfcc/chain.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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}

0 comments on commit 4fd1cf8

Please sign in to comment.