Skip to content

Commit b51b88d

Browse files
committed
Fix tags on broken SMT backend test
These various tests are either broken with error or timeout on SMT backends, in particular cprover-smt or z3.
1 parent 37499c0 commit b51b88d

File tree

10 files changed

+10
-10
lines changed

10 files changed

+10
-10
lines changed

regression/cbmc/Float-div3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33
--floatbv
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
1+
CORE broken-smt-backend
22
main.c
33

44
^\*\* Results:$

regression/cbmc/Quantifiers-assignment/test.desc

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-if/test.desc

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-initialisation2/test.desc

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-not-exists/fixed.desc

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-not/test.desc

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

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

44
^\*\* Results:$

regression/cbmc/union10/union_list2.desc

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

44
^EXIT=0$

regression/cbmc/union11/union_list.desc

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

44
^EXIT=0$

0 commit comments

Comments
 (0)