Enable SMT2 tests which pass with the overflow implementation

Author: thomasspriggs

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$

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$

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$

regression/cbmc/overflow/mod_overflow.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 mod_overflow.c
 --signed-overflow-check
 ^EXIT=10$

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$

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$

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$

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$

regression/cbmc/overflow/signed_multiplication1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 signed_multiplication1.c
 --signed-overflow-check
 ^EXIT=0$

regression/cbmc/overflow/signed_subtraction1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 signed_subtraction1.c
 --signed-overflow-check
 ^EXIT=0$

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$

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$

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$

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$