Run existing tests which now pass with SMT backend

thomasspriggs · thomasspriggs · commit 5032c15632ab · 2023-07-11T14:11:35.000+01:00
diff --git a/regression/cbmc/array-cell-sensitivity9/test.desc b/regression/cbmc/array-cell-sensitivity9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test.c
 --show-vcc
 main::1::array!0@1#2\[\[0\]\]..x =
diff --git a/regression/cbmc/array-cell-sensitivity9/test_execution.desc b/regression/cbmc/array-cell-sensitivity9/test_execution.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test.c
 
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/field-sensitivity-trace-wrong-counterexample-1/test.desc b/regression/cbmc/field-sensitivity-trace-wrong-counterexample-1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test.c
 --trace
 ^EXIT=10$
diff --git a/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc b/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc
@@ -1,4 +1,4 @@
-CORE smt-backend
+CORE smt-backend new-smt-backend
 singleton_interval_in_assume_7690.c
 --pointer-check
 ^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed (long|long long) int\)stk-\>top\]: SUCCESS$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE smt-backend`
	`1`	`+CORE smt-backend new-smt-backend`
`2`	`2`	`singleton_interval_in_assume_7690.c`
`3`	`3`	`--pointer-check`
`4`	`4`	`^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed (long\|long long) int\)stk-\>top\]: SUCCESS$`