Skip to content

Commit 43a86ca

Browse files
committed
Fix book regression tests handling of smt test runs
The `CMakeLists.txt` for the `book-examples` directory appears to be based on a copy of the one from the `regression/cbmc` directory. Unfortunately the first parameter to `add_test_pl_profile` needs to be unique and it has not been updated to a unique name for the new file. This was resulting in the existing tests not being run.
1 parent cf380d5 commit 43a86ca

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

regression/book-examples/CMakeLists.txt

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,15 +24,15 @@ add_test_pl_profile(
2424
)
2525

2626
add_test_pl_profile(
27-
"cbmc-cprover-smt2"
27+
"book-examples-cprover-smt2"
2828
"$<TARGET_FILE:cbmc> --cprover-smt2"
2929
"-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
3030
"CORE"
3131
)
3232

3333
# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
3434
add_test_pl_profile(
35-
"cbmc-new-smt-backend"
35+
"book-examples-new-smt-backend"
3636
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
3737
"${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
3838
"CORE"
@@ -41,7 +41,7 @@ add_test_pl_profile(
4141
# solver appears on the PATH in Windows already
4242
if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
4343
set_property(
44-
TEST "cbmc-cprover-smt2-CORE"
44+
TEST "book-examples-cprover-smt2-CORE"
4545
PROPERTY ENVIRONMENT
4646
"PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
4747
)

0 commit comments

Comments
 (0)