Skip to content

Commit 15da3ce

Browse files
committed
Change Makefile in regression/cbmc-incr-smt2 to support testing with multiple solvers.
Previously the command that was enabling the new SMT backend (and providing the script for invoking the appropriate SMT solver) was passed as part of the options passed in `test.desc`. Since this was removed, and passed as part of the test configuration in the `CMakeLists.txt`, we need to do the same here.
1 parent 6724efc commit 15da3ce

File tree

1 file changed

+7
-2
lines changed

1 file changed

+7
-2
lines changed

regression/cbmc-incr-smt2/Makefile

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,13 @@ else
99
exclude_broken_windows_tests=
1010
endif
1111

12-
test:
13-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
12+
test: ../test.pl test.z3
13+
14+
test.z3:
15+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
16+
17+
test.cvc5:
18+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang smt --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
1419

1520
tests.log: ../test.pl test
1621

0 commit comments

Comments
 (0)