Skip to content

Commit 43363a3

Browse files
tautschnigDaniel Kroening
authored and
Daniel Kroening
committed
Remove broken-smt-backend tag from passing tests
These pass at present. No attempt to bisect and link to the respective fixes has been made.
1 parent e85d6ba commit 43363a3

File tree

9 files changed

+11
-7
lines changed

9 files changed

+11
-7
lines changed

regression/cbmc/Anonymous_Struct3/test.desc

+1-1
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/Float13/test.desc

+1-1
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/Promotion3/test.desc

+1-1
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/Quantifiers-assertion/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33

44
^\*\* Results:$

regression/cbmc/Union_Initialization1/test.desc

+1-1
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-tests/test.desc

+2
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,5 @@ main.c
66
^VERIFICATION SUCCESSFUL$
77
--
88
^warning: ignoring
9+
--
10+
This test actually passes with the SMT2 back-end, but takes 88 seconds to do so.

regression/cbmc/graphml_witness1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--graphml-witness -
44
^EXIT=10$

regression/cbmc/union6/test.desc

+1-1
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/variable-access-to-constant-array/test.desc

+2
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,5 @@ main.c
66
^VERIFICATION FAILED$
77
--
88
^warning: ignoring
9+
This test actually passes when using the SMT2 back-end, but takes 68 seconds to
10+
do so.

0 commit comments

Comments
 (0)