Skip to content

Commit 293d469

Browse files
author
Thomas Kiley
committed
Update the help documention for min-unwind
It was somewhat ambiguous whether the checking started after N unwinds, or after N incremental solves. This documentation clarifies the checking is enabled after the Nth unwind, before the Nth solve.
1 parent 75cf803 commit 293d469

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/goto-checker/bmc_util.h

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -221,6 +221,11 @@ void run_property_decider(
221221
" of loop L\n" \
222222
" (use --show-loops to get the loop IDs)\n" \
223223
" --unwind-min nr start incremental-loop after nr unwindings\n" \
224+
" but before solving that iteration. If for\n" \
225+
" example it is 1, then the loop will be\n" \
226+
" unwound once, and immediately checked.\n" \
227+
" Note: this means for min-unwind 1 or\n"\
228+
" 0 all properties are checked.\n" \
224229
" --unwind-max nr stop incremental-loop after nr unwindings\n" \
225230
" --ignore-properties-before-unwind-min\n" \
226231
" do not check properties before unwind-min\n" \

0 commit comments

Comments
 (0)