Skip to content

Commit ae2e381

Browse files
committed
Relax property identity-number checks in enum_is_in_range test.
We are now producing more checks, which was messing with the expectations of the tests. Now made it a bit more general and all is good again.
1 parent bea1e88 commit ae2e381

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

regression/cbmc/enum_is_in_range/enum_test5.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ enum_test5.c
33
--enum-range-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main.enum-range-check.6\] line \d+ enum range check in ev3: SUCCESS$
7-
^\[main.enum-range-check.7\] line \d+ enum range check in ev2: FAILURE$
6+
^\[main.enum-range-check.\d\] line \d+ enum range check in ev3: SUCCESS$
7+
^\[main.enum-range-check.\d\] line \d+ enum range check in ev2: FAILURE$
88
--
9-
^\[main.enum-range-check.6\] line \d+ enum range check in ev3: FAILURE$
9+
^\[main.enum-range-check.\d\] line \d+ enum range check in ev3: FAILURE$
1010
^\*\*\*\* WARNING: no body for function __CPROVER_enum_is_in_range$
1111
--
1212
This test is for the enum_is_in_range working in assume statements

0 commit comments

Comments
 (0)