Skip to content

Commit 4b7cbff

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 436e544 commit 4b7cbff

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)