diffblue · NlightNFotis · Jan 20, 2023 · Dec 13, 2022
diff --git a/regression/cbmc/ACSL/quantifier-precedence.desc b/regression/cbmc/ACSL/quantifier-precedence.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 quantifier-precedence.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/ASHR1/test.desc b/regression/cbmc/ASHR1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Address_of1/test.desc b/regression/cbmc/Address_of1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --stop-on-fail
 ^\[main\.assertion

diff --git a/regression/cbmc/Address_of2/test.desc b/regression/cbmc/Address_of2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Access1/test.desc b/regression/cbmc/Array_Access1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Access2/test.desc b/regression/cbmc/Array_Access2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Access3/test.desc b/regression/cbmc/Array_Access3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Initialization1/test.desc b/regression/cbmc/Array_Initialization1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Initialization2/test.desc b/regression/cbmc/Array_Initialization2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Initialization3/test.desc b/regression/cbmc/Array_Initialization3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Pointer1/test.desc b/regression/cbmc/Array_Pointer1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Pointer2/test.desc b/regression/cbmc/Array_Pointer2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Pointer3/test.desc b/regression/cbmc/Array_Pointer3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Pointer4/test.desc b/regression/cbmc/Array_Pointer4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Pointer5/test.desc b/regression/cbmc/Array_Pointer5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Pointer6/test.desc b/regression/cbmc/Array_Pointer6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Pointer7/test.desc b/regression/cbmc/Array_Pointer7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_Propagation1/test.desc b/regression/cbmc/Array_Propagation1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Array_UF1/test.desc b/regression/cbmc/Array_UF1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 11
 ^EXIT=0$

diff --git a/regression/cbmc/Array_UF10/test.desc b/regression/cbmc/Array_UF10/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 1
 ^EXIT=0$

diff --git a/regression/cbmc/Array_UF11/test.desc b/regression/cbmc/Array_UF11/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 1
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF12/test.desc b/regression/cbmc/Array_UF12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 2
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF13/test.desc b/regression/cbmc/Array_UF13/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 1
 ^EXIT=0$

diff --git a/regression/cbmc/Array_UF14/test.desc b/regression/cbmc/Array_UF14/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 6
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF15/test.desc b/regression/cbmc/Array_UF15/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 11
 ^EXIT=0$

diff --git a/regression/cbmc/Array_UF16/test.desc b/regression/cbmc/Array_UF16/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 2
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF17/test.desc b/regression/cbmc/Array_UF17/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 9
 ^EXIT=0$

diff --git a/regression/cbmc/Array_UF18/test.desc b/regression/cbmc/Array_UF18/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 11
 ^EXIT=0$

diff --git a/regression/cbmc/Array_UF19/test.desc b/regression/cbmc/Array_UF19/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 3
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF2/test.desc b/regression/cbmc/Array_UF2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 5
 ^EXIT=0$

diff --git a/regression/cbmc/Array_UF20/test.desc b/regression/cbmc/Array_UF20/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 12
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF21/test.desc b/regression/cbmc/Array_UF21/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --bounds-check
 ^VERIFICATION FAILED$

diff --git a/regression/cbmc/Array_UF3/test.desc b/regression/cbmc/Array_UF3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 3 --no-unwinding-assertions
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF5/test.desc b/regression/cbmc/Array_UF5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 2
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF6/test.desc b/regression/cbmc/Array_UF6/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 3
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF7/test.desc b/regression/cbmc/Array_UF7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 3
 ^EXIT=10$

diff --git a/regression/cbmc/Array_UF9/test.desc b/regression/cbmc/Array_UF9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --arrays-uf-always --no-propagation --refine-arrays --unwind 21
 ^EXIT=10$

diff --git a/regression/cbmc/BV_Arithmetic1/test.desc b/regression/cbmc/BV_Arithmetic1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=10$

diff --git a/regression/cbmc/BV_Arithmetic2/test.desc b/regression/cbmc/BV_Arithmetic2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
  --unwind 32
 ^EXIT=0$

diff --git a/regression/cbmc/BV_Arithmetic3/test.desc b/regression/cbmc/BV_Arithmetic3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/BV_Arithmetic4/test.desc b/regression/cbmc/BV_Arithmetic4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
  --unwind 32
 ^EXIT=0$

diff --git a/regression/cbmc/BV_Arithmetic5/test.desc b/regression/cbmc/BV_Arithmetic5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
  --unwind 32
 ^EXIT=0$

diff --git a/regression/cbmc/BV_Arithmetic6/test.desc b/regression/cbmc/BV_Arithmetic6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Bitfields4/test.desc b/regression/cbmc/Bitfields4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Bool/bool1.desc b/regression/cbmc/Bool/bool1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 bool1.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Bool/bool4.desc b/regression/cbmc/Bool/bool4.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 bool4.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Bool/bool5-full-slice.desc b/regression/cbmc/Bool/bool5-full-slice.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 bool5.c
 --full-slice
 Generated 4 VCC\(s\), 0 remaining after simplification

diff --git a/regression/cbmc/Bool/bool5.desc b/regression/cbmc/Bool/bool5.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 bool5.c
 
 Generated 4 VCC\(s\), 0 remaining after simplification

diff --git a/regression/cbmc/Bool/bool6.desc b/regression/cbmc/Bool/bool6.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 bool6.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Boolean_Guards1/test.desc b/regression/cbmc/Boolean_Guards1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=0$

diff --git a/regression/cbmc/Division1/test.desc b/regression/cbmc/Division1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Division2/test.desc b/regression/cbmc/Division2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Ellipsis1/test.desc b/regression/cbmc/Ellipsis1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Ellipsis2/test.desc b/regression/cbmc/Ellipsis2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/End_thread1/test.desc b/regression/cbmc/End_thread1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Endianness1/test.desc b/regression/cbmc/Endianness1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
  --little-endian
 ^EXIT=0$

diff --git a/regression/cbmc/Endianness2/test.desc b/regression/cbmc/Endianness2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
  --big-endian
 ^EXIT=0$

diff --git a/regression/cbmc/Endianness3/test.desc b/regression/cbmc/Endianness3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
  --little-endian
 ^EXIT=0$

diff --git a/regression/cbmc/Endianness4/test.desc b/regression/cbmc/Endianness4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 
 ^EXIT=0$

diff --git a/regression/cbmc/Endianness5/test.desc b/regression/cbmc/Endianness5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --little-endian --pointer-check
 ^EXIT=0$

diff --git a/regression/cbmc/Endianness6/test.desc b/regression/cbmc/Endianness6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --big-endian
 ^EXIT=0$

diff --git a/regression/cbmc/Endianness8/test.desc b/regression/cbmc/Endianness8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --big-endian
 ^EXIT=0$

diff --git a/regression/cbmc/Endianness9/test.desc b/regression/cbmc/Endianness9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --big-endian
 ^EXIT=0$

diff --git a/regression/cbmc/Error_Label1/test.desc b/regression/cbmc/Error_Label1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --error-label ERROR
 ^EXIT=10$

diff --git a/regression/cbmc/Error_Label2/test.desc b/regression/cbmc/Error_Label2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --error-label ERROR --no-assertions
 ^EXIT=10$

diff --git a/regression/cbmc/Error_Label3/test.desc b/regression/cbmc/Error_Label3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --error-label ERROR1 --error-label ERROR2
 ^EXIT=10$