Enable SMT2 tests which pass with the overflow implementation

thomasspriggs · thomasspriggs · commit 40dcadc39f62 · 2022-03-18T11:28:31.000Z
diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 signed_overflow.c
 --incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/overflow/leftshift_overflow-c89.desc b/regression/cbmc/overflow/leftshift_overflow-c89.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 leftshift_overflow.c
 --signed-overflow-check --c89
 ^EXIT=10$
diff --git a/regression/cbmc/overflow/leftshift_overflow-c99.desc b/regression/cbmc/overflow/leftshift_overflow-c99.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 leftshift_overflow.c
 --signed-overflow-check --c99
 ^EXIT=10$
diff --git a/regression/cbmc/overflow/mod_overflow.desc b/regression/cbmc/overflow/mod_overflow.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 mod_overflow.c
 --signed-overflow-check
 ^EXIT=10$
diff --git a/regression/cbmc/overflow/signed_addition_overflow1.desc b/regression/cbmc/overflow/signed_addition_overflow1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 signed_addition_overflow1.c
 --signed-overflow-check
 ^EXIT=10$
diff --git a/regression/cbmc/overflow/signed_addition_overflow2.desc b/regression/cbmc/overflow/signed_addition_overflow2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 signed_addition_overflow2.c
 --signed-overflow-check
 ^EXIT=10$
diff --git a/regression/cbmc/overflow/signed_addition_overflow3.desc b/regression/cbmc/overflow/signed_addition_overflow3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 signed_addition_overflow3.c
 --signed-overflow-check --conversion-check
 ^EXIT=10$
diff --git a/regression/cbmc/overflow/signed_addition_overflow4.desc b/regression/cbmc/overflow/signed_addition_overflow4.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 signed_addition_overflow4.c
 --signed-overflow-check --conversion-check
 ^EXIT=10$
diff --git a/regression/cbmc/overflow/signed_multiplication1.desc b/regression/cbmc/overflow/signed_multiplication1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 signed_multiplication1.c
 --signed-overflow-check
 ^EXIT=0$
diff --git a/regression/cbmc/overflow/signed_subtraction1.desc b/regression/cbmc/overflow/signed_subtraction1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 signed_subtraction1.c
 --signed-overflow-check
 ^EXIT=0$
diff --git a/regression/cbmc/overflow/unary_minus_overflow.desc b/regression/cbmc/overflow/unary_minus_overflow.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 unary_minus_overflow.c
 --signed-overflow-check --unsigned-overflow-check
 ^EXIT=10$
diff --git a/regression/cbmc/pragma_cprover2/test.desc b/regression/cbmc/pragma_cprover2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --signed-overflow-check
 ^\[main.overflow\.1\] line 21 arithmetic overflow on signed \+ in n \+ n: FAILURE$
diff --git a/regression/cbmc/set-property-inline1/test.desc b/regression/cbmc/set-property-inline1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --property inc.overflow.1 --property inc.overflow.2 --slice-formula --signed-overflow-check --conversion-check
 ^EXIT=10$
diff --git a/regression/contracts/variant_init_inside_loop/test.desc b/regression/contracts/variant_init_inside_loop/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --apply-loop-contracts _ --unsigned-overflow-check
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+CORE`
`2`	`2`	`signed_overflow.c`
`3`	`3`	`--incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace`
`4`	`4`	`^VERIFICATION FAILED$`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE new-smt-backend`
`2`	`2`	`leftshift_overflow.c`
`3`	`3`	`--signed-overflow-check --c89`
`4`	`4`	`^EXIT=10$`