Skip to content

Commit 86e159a

Browse files
committed
More tests adjusted
1 parent a810101 commit 86e159a

File tree

3 files changed

+5
-3
lines changed

3 files changed

+5
-3
lines changed

regression/cbmc/Float-div2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE broken-z3-smt-backend no-new-smt
22
main.c
3-
--floatbv
3+
--floatbv --no-built-in-assertions
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

regression/cbmc/Float-div3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE broken-z3-smt-backend no-new-smt
22
main.c
3-
--floatbv
3+
--floatbv --no-built-in-assertions
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

regression/cbmc/pragma_cprover_enable2/test.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,9 @@ main.c
66
^\[main\.overflow\.3\] line 15 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
77
^\[main\.overflow\.4\] line 16 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
88
^\[main\.overflow\.5\] line 17 arithmetic overflow on signed \+ in x \+ n: FAILURE$
9-
^\*\* 5 of \d+ failed
9+
^\[main\.overflow\.6\] line 20 arithmetic overflow on signed \+ in n \+ n: FAILURE$
10+
^\[main\.overflow\.7\] line 21 arithmetic overflow on signed \+ in x \+ n: FAILURE$
11+
^\*\* 7 of \d+ failed
1012
^VERIFICATION FAILED$
1113
^EXIT=10$
1214
^SIGNAL=0$

0 commit comments

Comments
 (0)