Merge pull request #7950 from thomasspriggs/tas/fix_book_examples_smt

Fix book regression tests handling of smt test runs

Author: thomasspriggs

regression/book-examples/CMakeLists.txt

@@ -24,15 +24,15 @@ add_test_pl_profile(
 )
 
 add_test_pl_profile(
-    "cbmc-cprover-smt2"
+    "book-examples-cprover-smt2"
     "$<TARGET_FILE:cbmc> --cprover-smt2"
     "-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}"
     "CORE"
 )
 
 # If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
 add_test_pl_profile(
-  "cbmc-new-smt-backend"
+  "book-examples-new-smt-backend"
   "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
   "${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
   "CORE"
@@ -41,7 +41,7 @@ add_test_pl_profile(
 # solver appears on the PATH in Windows already
 if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
   set_property(
-    TEST "cbmc-cprover-smt2-CORE"
+    TEST "book-examples-cprover-smt2-CORE"
     PROPERTY ENVIRONMENT
       "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
   )

regression/book-examples/abs/C1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 abs.c
 --function abs
 ^EXIT=0$

regression/book-examples/abs/C13.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 abs.c
 --function abs --signed-overflow-check --show-goto-functions
 ^EXIT=0$

regression/book-examples/abs/C2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 abs.c
 --function abs --signed-overflow-check
 ^EXIT=10$

regression/book-examples/abs/C3.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 abs.c
 --function abs --signed-overflow-check --trace
 ^EXIT=10$

regression/book-examples/binsearch/C4.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 binsearch.c
 --function binsearch --unwind 6 --bounds-check --unwinding-assertions
 ^EXIT=0$

regression/book-examples/lock/depth.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 lock.c
 --depth 10
 ^EXIT=0$

regression/book-examples/lock/unwind1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 lock.c
 --unwind 1
 ^EXIT=0$

regression/book-examples/lock/unwind2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 lock.c
 --unwind 2
 ^EXIT=10$

regression/book-examples/login/C5.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 login.c
 --unwind 20 --bounds-check
 ^EXIT=10$

regression/book-examples/login/C6.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 login.c
 --show-properties --bounds-check --pointer-check
 ^EXIT=0$

regression/book-examples/login/C7.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 login.c
 --unwind 20 --show-vcc --bounds-check --pointer-check
 ^EXIT=0$

regression/book-examples/login/C8.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 login.c
 --unwind 20 --bounds-check --pointer-check
 ^EXIT=10$

regression/book-examples/login/C9.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 login.c
 --unwind 20 --bounds-check --pointer-check --trace
 ^EXIT=10$