Skip to content

Commit d91d9d9

Browse files
committed
Add tests for traces in one-loop checker
1: working test for the standard trace. 2: failing test for the beautified shortest trace.
1 parent 07e3177 commit d91d9d9

File tree

2 files changed

+22
-0
lines changed

2 files changed

+22
-0
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
KNOWNBUG
2+
main.c
3+
--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --trace --beautify --no-sat-preprocessor --stop-on-fail
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
^State \d+ file main.c function havocIO line 501 thread \d+$
8+
--
9+
^warning: ignoring
10+
--
11+
This will fail the invariant on `build_goto_trace.cpp:320` asserting certain
12+
properties of the last trace step. It is possible this combination of options is
13+
incompatible.
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --trace
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
^State \d+ file main.c function havocIO line 501 thread \d+$
8+
--
9+
^warning: ignoring

0 commit comments

Comments
 (0)