Skip to content

Commit 0b8ebc1

Browse files
committed
Add a test.pl profile to run new tests under the new SMT backend.
This defaults to running only tests marked with an a specific label, `new-smt-backend`. For now, no tests have been marked so, so this new configuration runs zero tests (skips everything).
1 parent de9fa65 commit 0b8ebc1

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

regression/cbmc/CMakeLists.txt

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,14 @@ add_test_pl_profile(
2424
"CORE"
2525
)
2626

27+
# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
28+
add_test_pl_profile(
29+
"cbmc-new-smt-backend"
30+
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula"
31+
"-I;new-smt-backend;-s;new-smt-backend"
32+
"CORE"
33+
)
34+
2735
# solver appears on the PATH in Windows already
2836
if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
2937
set_property(

0 commit comments

Comments
 (0)