Skip to content

Commit cdbc539

Browse files
TGWDBNlightNFotis
authored andcommitted
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 ddbe35b commit cdbc539

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)