Remove broken-smt-backend tags where tests currently pass

No bisecting was done, but the tests appear to work fine at present.

Author: tautschnig

regression/cbmc/Array_operations1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$

regression/cbmc/Float-equality1/test_no_equality.desc

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

regression/cbmc/array-cell-sensitivity7/test_execution.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/array-cell-sensitivity8/test_execution.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/byte_update12/test.desc

@@ -6,3 +6,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test fails with the CPROVER SMT2 solver on Ubuntu 18.04 only.

regression/cbmc/byte_update14/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 
 ^VERIFICATION FAILED$

regression/cbmc/compact-trace/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --compact-trace
 activate-multi-line-match

regression/cbmc/gcc_vector1/test.desc

@@ -6,3 +6,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test fails with the CPROVER SMT2 solver on Ubuntu 18.04 only.

regression/cbmc/gcc_vector3/test.desc

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

regression/cbmc/json-interface1/test_wrong_flag.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 --json-interface
 < test_wrong_flag.json
 ^EXIT=6$

regression/cbmc/json-interface1/test_wrong_option.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 --json-interface
 < test_wrong_option.json
 ^EXIT=6$

regression/cbmc/memory_allocation1/test.desc

@@ -10,3 +10,5 @@ main.c
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
+This test fails with the CPROVER SMT2 solver on Windows only.

regression/cbmc/printf1/test.desc

@@ -9,3 +9,5 @@ main.c
 ^PRINT f1 123\.000000, -123\.000000, 123\.123000, 0\.123000$
 --
 ^warning: ignoring
+--
+This test fails with the CPROVER SMT2 solver on Windows only.

regression/cbmc/stack-trace/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --stack-trace
 activate-multi-line-match

regression/cbmc/union12/test.desc

@@ -13,3 +13,5 @@ Despite the large array inside the union, the test should complete within 10
 seconds. Simplify extractbits(concatenation(...)) is essential to make this
 possible. With 77236cc34 (Avoid nesting of ID_with/byte_update by rewriting
 byte_extract to use the root object) the test already is trivial, however.
+
+This test fails with the CPROVER SMT2 solver on Windows only.

regression/cbmc/union15/test.desc

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

regression/cbmc/union6/test.desc

@@ -1,11 +1,8 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
---
-This test reports a VERIFICATION ERROR when running with the SMT2 solver on
-Windows only.

regression/cbmc/union7/test.desc

@@ -1,11 +1,8 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
---
-This test reports a VERIFICATION ERROR when running with the SMT2 solver on
-Windows only.

regression/cbmc/va_list2/test.desc

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

regression/cbmc/va_list3/test.desc

@@ -6,3 +6,5 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test fails with the CPROVER SMT2 solver on Windows only.

regression/cbmc/variable-access-to-constant-array/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$
@@ -7,9 +7,6 @@ main.c
 --
 ^warning: ignoring
 --
-This test actually passes when using the SMT2 back-end, but takes 68 seconds to
-do so.
-
 Field-sensitive encoding of array accesses for an array of 2^16 elements is very
 expensive. We might consider some bounds up to which we actually do field
 expansion, or at least need to mark this test as "THOROUGH."