--base-k-step 0 causes unbounded unwinding #6093

Hi @MarkAA-uw, thanks for the report — and thanks @lucasccordeiro for the ping. This one is a real bug; fix is up in #6102.

Root cause: --base-k-step 0 starts the base case at k = 0, and the k-induction driver derives the unwind bound from k (so it runs --unwind 0 here). ESBMC treats --unwind 0 as unlimited unwinding — loop termination is gated on max_unwind != 0 && unwind >= max_unwind — so max_unwind == 0 never stops a loop and the base case unwinds forever, ignoring --max-k-step. The existing validation only checked base-k-step < max-k-step, so 0 slipped through.

Fix: --base-k-step 0 is now rejected up front with a clear error. The base case must start at k >= 1, because k = 0 cannot be represented as an unwind bound (0 is the "unlimited" sentinel). Use --base-k-step 1 (the default) for a bounded sweep.

@LukeW1999 -
Thanks!
-mark