Merge pull request #6714 from NlightNFotis/add_new_smt_backend_label_to_regression_tests

Add new smt backend label to regression tests

Author: NlightNFotis

regression/cbmc/Associativity1/test.desc

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

regression/cbmc/Assumption1/test.desc

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

regression/cbmc/Bitfields2/test.desc

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

regression/cbmc/CMakeLists.txt

@@ -24,6 +24,14 @@ add_test_pl_profile(
     "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"
+  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula"
+  "-I;new-smt-backend;-s;new-smt-backend"
+  "CORE"
+)
+
 # solver appears on the PATH in Windows already
 if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
   set_property(

regression/cbmc/Fixedbv1/test.desc

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

regression/cbmc/Fixedbv2/test.desc

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

regression/cbmc/Fixedbv4/test.desc

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

regression/cbmc/Fixedbv6/test.desc

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

regression/cbmc/Fixedbv8/test.desc

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

regression/cbmc/Function-KnR1/test.desc

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

regression/cbmc/Function1/test.desc

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

regression/cbmc/Function10/test.desc

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

regression/cbmc/Function11/test.desc

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

regression/cbmc/Function13/test.desc

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

regression/cbmc/Function14/test.desc

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

regression/cbmc/Function6/test.desc

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

regression/cbmc/Function7/test.desc

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

regression/cbmc/Function8/test.desc

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

regression/cbmc/Function9/test.desc

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

regression/cbmc/Function_Pointer5/test.desc

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

regression/cbmc/Makefile

@@ -29,6 +29,11 @@ test-paths-lifo:
 					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
 					  -s paths-lifo $(GCC_ONLY)
 
+test-new-smt-backend:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula" \
+					  -I new-smt-backend \
+					  -s new-smt-backend $(GCC_ONLY)
+
 tests.log: ../test.pl test
 
 clean:

regression/cbmc/Mod1/test.desc

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

regression/cbmc/Mod2/test.desc

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

regression/cbmc/Negation1/test.desc

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

regression/cbmc/Negation2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-propagation
 ^EXIT=0$

regression/cbmc/Nondet1/test.desc

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

regression/cbmc/always_inline1/test.desc

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

regression/cbmc/assert_func_four/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 function .* is not declared

regression/cbmc/assert_lhs/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 function .* is not declared

regression/cbmc/assert_one/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 function .* is not declared

regression/cbmc/char1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --unsigned-char
 ^EXIT=0$

regression/cbmc/cprover_assert_two/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=6$

regression/cbmc/exit1/test.desc

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

regression/cbmc/for1/test.desc

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

regression/cbmc/for2/test.desc

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

regression/cbmc/for3/test.desc

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

regression/cbmc/goto1/test.desc

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

regression/cbmc/goto4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --unwind 1 --unwinding-assertions
 ^EXIT=10$

regression/cbmc/guard1/test.desc

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

regression/cbmc/if1/test.desc

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

regression/cbmc/if3/test.desc

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

regression/cbmc/if4/test.desc

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

regression/cbmc/no-propagation/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-propagation
 Generated 1 VCC\(s\), 1 remaining after simplification

regression/cbmc/noop1/test.desc

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

regression/cbmc/null1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify
 ^EXIT=0$

regression/cbmc/null4/test.desc

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

regression/cbmc/r_w_ok4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/return1/test.desc

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

regression/cbmc/return3/test.desc

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

regression/cbmc/return4/test.desc

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

regression/cbmc/return5/test.desc

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