Run additional regressions with new SMT solver

This commit adds 130 tests from regression/cbmc to the list of tests
that is run with the new incremental SMT2 solver.

Notice that some tests are related to unsupported features, that
however are removed by the simplification steps before the solver is
invoked making them tractable.

Author: Enrico Steffinlongo

regression/cbmc/Array_UF21/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --arrays-uf-always --bounds-check
 ^VERIFICATION FAILED$

regression/cbmc/Float-equality2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 (Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)

regression/cbmc/Float-overflow1/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --floatbv --float-overflow-check
 ^EXIT=0$

regression/cbmc/Float-overflow2/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --floatbv --float-overflow-check
 ^EXIT=10$

regression/cbmc/Float-rounding/compile_time_rounding.desc

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

regression/cbmc/Float1/test.desc

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

regression/cbmc/Float11/test.desc

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

regression/cbmc/Float13/test.desc

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

regression/cbmc/Float14/test.desc

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

regression/cbmc/Float2/test.desc

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