File tree Expand file tree Collapse file tree 2 files changed +10
-4
lines changed
regression/cbmc-incr-oneloop Expand file tree Collapse file tree 2 files changed +10
-4
lines changed Original file line number Diff line number Diff line change 1
- CORE
1
+ FUTURE
2
2
main.c
3
- --incremental-loop main.0 --stop-when-unsat
3
+ --incremental-loop main.0 --stop-when-pass
4
4
^EXIT=0$
5
5
^SIGNAL=0$
6
6
^VERIFICATION SUCCESSFUL$
7
7
--
8
8
^warning: ignoring
9
+ --
10
+ Step case of k-induction for a single loop:
11
+ incrementally try for increasing k as long as there are failing assertions.
Original file line number Diff line number Diff line change 1
- CORE
1
+ FUTURE
2
2
main.c
3
- --incremental-loop main.0 --stop-when-unsat
3
+ --incremental-loop main.0 --stop-when-pass
4
4
^EXIT=0$
5
5
^SIGNAL=0$
6
6
^VERIFICATION SUCCESSFUL$
7
7
--
8
8
^warning: ignoring
9
+ --
10
+ Step case of k-induction for a single loop:
11
+ incrementally try for increasing k as long as there are failing assertions.
You can’t perform that action at this time.
0 commit comments