Skip to content

Commit 41f6d5a

Browse files
committed
Remove broken-smt-backend tags where tests currently pass
No bisecting was done, but the tests appear to work fine at present.
1 parent 25a7b36 commit 41f6d5a

File tree

19 files changed

+19
-19
lines changed

19 files changed

+19
-19
lines changed

regression/cbmc/Array_operations1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=10$

regression/cbmc/Float-equality1/test_no_equality.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
test.c
33

44
^VERIFICATION FAILED$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
test.c
33

44
^VERIFICATION FAILED$

regression/cbmc/byte_update14/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
test.c
33

44
^VERIFICATION FAILED$

regression/cbmc/compact-trace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--compact-trace
44
activate-multi-line-match

regression/cbmc/gcc_vector3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc/json-interface1/test_wrong_flag.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
--json-interface
33
< test_wrong_flag.json
44
^EXIT=6$

regression/cbmc/json-interface1/test_wrong_option.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
--json-interface
33
< test_wrong_option.json
44
^EXIT=6$

regression/cbmc/null6/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=10$

regression/cbmc/pointer-primitive-check-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--pointer-primitive-check
44
^EXIT=10$

regression/cbmc/pointer-primitive-check-04/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--pointer-primitive-check
44
^EXIT=10$

regression/cbmc/stack-trace/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--stack-trace
44
activate-multi-line-match

regression/cbmc/union15/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc/union6/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--little-endian
44
^EXIT=0$

regression/cbmc/union7/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--big-endian
44
^EXIT=0$

regression/cbmc/va_list2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=10$

regression/cbmc/void_pointer4/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^EXIT=10$

0 commit comments

Comments
 (0)