Skip to content

Commit 96898d4

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. # Please enter the commit message for your changes. Lines starting
1 parent 53c744a commit 96898d4

File tree

10 files changed

+10
-10
lines changed

10 files changed

+10
-10
lines changed

regression/cbmc/Float-div3/test.desc

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

regression/cbmc/Quantifiers-assertion/test.desc

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-assignment/test.desc

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-if/test.desc

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-initialisation2/test.desc

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

44
^\*\* Results:$

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

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

44
^\*\* Results:$

regression/cbmc/Quantifiers-not/test.desc

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

44
^\*\* Results:$

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

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

44
^\*\* Results:$

regression/cbmc/union10/union_list2.desc

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

44
^EXIT=0$

regression/cbmc/union11/union_list.desc

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

44
^EXIT=0$

0 commit comments

Comments
 (0)