We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 07e3177 commit 39c5ac8Copy full SHA for 39c5ac8
regression/cbmc-incr-oneloop/alarm2/fancy_trace_test.desc
@@ -0,0 +1,12 @@
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
+--
8
+^warning: ignoring
9
10
+This will fail the invariant on `build_goto_trace.cpp:320` asserting certain
11
+properties of the last trace step. It is possible this combination of options is
12
+incompatible.
regression/cbmc-incr-oneloop/alarm2/trace_test.desc
@@ -0,0 +1,9 @@
+CORE
+--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --trace
+^State \d+ file main.c function havocIO line 501 thread \d+$
0 commit comments