Update test runner replace new-smt-backend with no-new-smt

In order to make the tags in the previous commit work as expected.

Author: thomasspriggs

regression/book-examples/CMakeLists.txt

@@ -30,11 +30,11 @@ add_test_pl_profile(
     "CORE"
 )
 
-# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+# If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
 add_test_pl_profile(
   "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"
+  "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )
 

regression/book-examples/Makefile

@@ -31,7 +31,7 @@ test-paths-lifo:
 
 test-new-smt-backend:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
-					  -I new-smt-backend \
+					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)
 
 tests.log: ../test.pl test

regression/cbmc-primitives/CMakeLists.txt

@@ -5,11 +5,11 @@ if(Z3_EXISTS)
         "$<TARGET_FILE:cbmc>"
     )
 
-    # If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+    # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
     add_test_pl_profile(
             "cbmc-primitives-new-smt-backend"
             "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-            "-I;new-smt-backend;-s;new-smt-backend"
+            "-X;no-new-smt;-s;new-smt-backend"
             "CORE"
     )
 else()

regression/cbmc-primitives/Makefile

@@ -4,7 +4,7 @@ test:
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 test.smt2_incr:
-	@../test.pl -e -p -I new-smt-backend -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -X no-new-smt -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc

regression/cbmc/CMakeLists.txt

@@ -30,11 +30,11 @@ add_test_pl_profile(
     "CORE"
 )
 
-# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
+# If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
 add_test_pl_profile(
   "cbmc-new-smt-backend"
   "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
-  "${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
+  "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )
 

regression/cbmc/Makefile

@@ -31,7 +31,7 @@ test-paths-lifo:
 
 test-new-smt-backend:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
-					  -I new-smt-backend \
+					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)
 
 tests.log: ../test.pl test