Remove broken-smt-backend tags where tests currently pass

tautschnig · tautschnig · commit 37643e2713ab · 2021-04-01T19:20:13.000Z
No bisecting was done, but the tests appear to work fine at present.
diff --git a/regression/cbmc/Array_operations1/test.desc b/regression/cbmc/Array_operations1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Float-equality1/test_no_equality.desc b/regression/cbmc/Float-equality1/test_no_equality.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp5/test.desc b/regression/cbmc/Float-no-simp5/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float22/test.desc b/regression/cbmc/Float22/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Promotion3/test.desc b/regression/cbmc/Promotion3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/array-cell-sensitivity7/test_execution.desc b/regression/cbmc/array-cell-sensitivity7/test_execution.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/array-cell-sensitivity8/test_execution.desc b/regression/cbmc/array-cell-sensitivity8/test_execution.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/byte_update12/test.desc b/regression/cbmc/byte_update12/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update14/test.desc b/regression/cbmc/byte_update14/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test.c
 
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --compact-trace
 activate-multi-line-match
diff --git a/regression/cbmc/gcc_vector1/test.desc b/regression/cbmc/gcc_vector1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/gcc_vector3/test.desc b/regression/cbmc/gcc_vector3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/json-interface1/test_wrong_flag.desc b/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$
diff --git a/regression/cbmc/json-interface1/test_wrong_option.desc b/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$
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/printf1/test.desc b/regression/cbmc/printf1/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --trace
 ^EXIT=10$
diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --stack-trace
 activate-multi-line-match
diff --git a/regression/cbmc/union15/test.desc b/regression/cbmc/union15/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/union6/test.desc b/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.
diff --git a/regression/cbmc/va_list2/test.desc b/regression/cbmc/va_list2/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/va_list3/test.desc b/regression/cbmc/va_list3/test.desc
@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/variable-access-to-constant-array/test.desc b/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."

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE broken-smt-backend`
	`1`	`+CORE`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=10$`