Skip to content

Commit f2268c6

Browse files
committed
Mark flaky fault-localization test as FUTURE
The test will sometimes pass, depending on what model the solver produces. When such a passing model happens to be is produced, it breaks our checking of "KNOWNBUG" tests.
1 parent 8560cdc commit f2268c6

File tree

1 file changed

+4
-2
lines changed
  • regression/cbmc/fault_localization-all_properties2

1 file changed

+4
-2
lines changed
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
FUTURE
22
main.c
33
--localize-faults
44
^EXIT=10$
@@ -8,4 +8,6 @@ line 9 function main$
88
--
99
--
1010
CBMC wrongly reports line 7 as the faulty statement when instead it should be
11-
line 9.
11+
line 9. The test is marked as "FUTURE" as it will sometimes pass, depending on
12+
what model the solver produces. It would, therefore, break our checking of
13+
"KNOWNBUG" tests.

0 commit comments

Comments
 (0)