Add a broken-smt-backend tag to regression test

tautschnig · tautschnig · commit ea9689ff7f93 · 2019-02-07T17:58:13.000Z
This will enable dropping the script that deletes directories, and thus makes it
easier to repeated build&amp;test runs.
diff --git a/regression/cbmc/Anonymous_Struct3/test.desc b/regression/cbmc/Anonymous_Struct3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Array_operations1/test.desc b/regression/cbmc/Array_operations1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Bitfields3/paths.desc b/regression/cbmc/Bitfields3/paths.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --bounds-check --paths lifo
 ^EXIT=0$
diff --git a/regression/cbmc/Bitfields3/test.desc b/regression/cbmc/Bitfields3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc/Empty_struct1/test.desc b/regression/cbmc/Empty_struct1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Endianness4/test.desc b/regression/cbmc/Endianness4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Endianness6/test.desc b/regression/cbmc/Endianness6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --big-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Float-div2/test.desc b/regression/cbmc/Float-div2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-div3/test.desc b/regression/cbmc/Float-div3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp1/test.desc b/regression/cbmc/Float-no-simp1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp2/test.desc b/regression/cbmc/Float-no-simp2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp3/test.desc b/regression/cbmc/Float-no-simp3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp4/test.desc b/regression/cbmc/Float-no-simp4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^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
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp6/test.desc b/regression/cbmc/Float-no-simp6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp7/test.desc b/regression/cbmc/Float-no-simp7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-smt2-1/test.desc b/regression/cbmc/Float-smt2-1/test.desc
@@ -1,4 +1,4 @@
-CORE smt-backend
+CORE smt-backend broken-smt-backend
 main.c
 --smt2
 ^EXIT=10$
diff --git a/regression/cbmc/Float-to-double2/test.desc b/regression/cbmc/Float-to-double2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int1/test.desc b/regression/cbmc/Float-to-int1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int2/test.desc b/regression/cbmc/Float-to-int2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int3/test.desc b/regression/cbmc/Float-to-int3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-zero-sum1/test.desc b/regression/cbmc/Float-zero-sum1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float12/test.desc b/regression/cbmc/Float12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float13/test.desc b/regression/cbmc/Float13/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float20/test.desc b/regression/cbmc/Float20/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float22/test.desc b/regression/cbmc/Float22/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float23/test.desc b/regression/cbmc/Float23/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float3/test.desc b/regression/cbmc/Float3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float4/test.desc b/regression/cbmc/Float4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float5/test.desc b/regression/cbmc/Float5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float6/test.desc b/regression/cbmc/Float6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float8/test.desc b/regression/cbmc/Float8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Linking4/test.desc b/regression/cbmc/Linking4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 link1.c
 link2.c
 ^EXIT=0$
diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 module2.c
 ^EXIT=10$
diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 module.c
 ^EXIT=10$
diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/Multi_Dimensional_Array2/test.desc b/regression/cbmc/Multi_Dimensional_Array2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic11/test.desc b/regression/cbmc/Pointer_Arithmetic11/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Promotion3/test.desc b/regression/cbmc/Promotion3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Union_Initialization1/test.desc b/regression/cbmc/Union_Initialization1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths broken-smt-backend
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects
diff --git a/regression/cbmc/array-function-parameters/test.desc b/regression/cbmc/array-function-parameters/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check
 \[test.assertion.1\] line \d+ assertion Test.lists\[0\]->next: SUCCESS
diff --git a/regression/cbmc/array-tests/test.desc b/regression/cbmc/array-tests/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/byte_update2/test.desc b/regression/cbmc/byte_update2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update4/test.desc b/regression/cbmc/byte_update4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update6/test.desc b/regression/cbmc/byte_update6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update7/test.desc b/regression/cbmc/byte_update7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update8/test.desc b/regression/cbmc/byte_update8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update9/test.desc b/regression/cbmc/byte_update9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --big-endian
 ^EXIT=0$
diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --compact-trace
 activate-multi-line-match
diff --git a/regression/cbmc/dynamic_size1/stack_object.desc b/regression/cbmc/dynamic_size1/stack_object.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 stack_object.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --graphml-witness -
 ^EXIT=10$
diff --git a/regression/cbmc/integer-assignments1/test.desc b/regression/cbmc/integer-assignments1/test.desc
@@ -1,4 +1,4 @@
-CORE smt-backend
+CORE smt-backend broken-smt-backend
 main.c
 --trace --smt2
 ^EXIT=10$
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc
diff --git a/regression/cbmc/scanf1/test.desc b/regression/cbmc/scanf1/test.desc
diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc
diff --git a/regression/cbmc/struct6/test.desc b/regression/cbmc/struct6/test.desc
diff --git a/regression/cbmc/struct7/test.desc b/regression/cbmc/struct7/test.desc
diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
diff --git a/regression/cbmc/trace_show_function_calls/test.desc b/regression/cbmc/trace_show_function_calls/test.desc
diff --git a/regression/cbmc/uninterpreted_function/uf1.desc b/regression/cbmc/uninterpreted_function/uf1.desc
diff --git a/regression/cbmc/uninterpreted_function/uf2.desc b/regression/cbmc/uninterpreted_function/uf2.desc
diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc
diff --git a/regression/cbmc/union6/test.desc b/regression/cbmc/union6/test.desc
diff --git a/regression/cbmc/union7/test.desc b/regression/cbmc/union7/test.desc
diff --git a/regression/cbmc/union9/test.desc b/regression/cbmc/union9/test.desc
diff --git a/regression/cbmc/variable-access-to-constant-array/test.desc b/regression/cbmc/variable-access-to-constant-array/test.desc
diff --git a/regression/cbmc/void_pointer2/test.desc b/regression/cbmc/void_pointer2/test.desc
diff --git a/regression/cbmc/void_pointer3/test.desc b/regression/cbmc/void_pointer3/test.desc
diff --git a/regression/cbmc/void_pointer4/test.desc b/regression/cbmc/void_pointer4/test.desc

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