Loop Invariants

esbmc file.c --loop-invariant

ESBMC supports user-provided loop invariants as an alternative to expensive loop unwinding. This is particularly beneficial for programs with large loop bounds or unbounded loops, where traditional k-induction may become computationally prohibitive or hit iteration limits.

Like function contracts, loop invariants are expressed with built-in constructs placed in the source. The core construct is __ESBMC_loop_invariant(condition), placed before the loop as a statement ending with ;.

Choosing a Mode

ESBMC provides two distinct modes, and picking the wrong one is the most common reason a correct invariant appears not to help. The deciding question is what your post-loop property needs in order to follow:

The second row is easy to miss. An invariant like i <= N && sum == i * 10 only yields sum == N * 10 once you also know !(i < N), i.e. i == N at exit. That final step is exit reasoning, and only --loop-invariant-check performs it. Under --loop-invariant such a property falls back to bounded unrolling and will report VERIFICATION UNKNOWN once the bound exceeds the k-induction step limit.

Properties over an array filled by the loop — __ESBMC_forall(&i, !(i < N) || p[i] == 0) and friends — are almost always in the second row, since they need i == N at exit.

Verification Modes

--loop-invariant — Combined Mode

Integrates invariant checking with k-induction. The invariant is used as an assumption that strengthens the inductive step, so whenever the property follows from the invariant alone, verification closes at a small k regardless of how large the loop bound is.

Note: --loop-invariant implicitly enables k-induction. No extra flags are required.

How it works — two-branch transformation:

IF !nondet_bool() GOTO loop_head       // Non-deterministically skip to Branch 2

// --- Branch 1: Inductivity Check ---
ASSERT(INV)                            // Base case: invariant holds on entry
HAVOC(loop_vars)
ASSUME(INV)
ASSUME(loop_entry_cond)
ASSERT(INV)                            // Inductive step: invariant still holds
ASSUME(false)                          // Terminate Branch 1

loop_head:
// --- Branch 2: K-Induction ---
ASSUME(INV)                            // Use invariant as a hint for k-induction
GOTO loop_head

Expected outcomes:

The last row holds when the property follows from the invariant alone. If it also needs the negated loop condition, the inductive step cannot close and k-induction falls back to unrolling — see Choosing a Mode.

--loop-invariant-check — Havoc Abstraction Mode

Applies the classic Hoare rule, replacing the annotated loop with:

1. Base-case assertion — invariant holds on entry
2. Havoc + Assume — abstracts the loop body nondeterministically
3. Inductive-step assertion — invariant still holds after one iteration

The loop is then cut, so this mode avoids loop unrolling entirely and its cost does not grow with the loop bound. It is the only mode that performs exit reasoning (invariant && !condition at the loop exit), which makes it the required choice for the second row of Choosing a Mode.

Three caveats:

• A claim after the loop is checked against the abstraction, not against the program, so a correct but too weak invariant admits states the program cannot reach. Such a claim is reported UNKNOWN rather than FAILED, with the reason attached — an over-approximation can prove a claim, never refute it:

  ** Results:
  main.c, function main
    PASSED   [main.assertion.1]  line 11  loop invariant base case
    PASSED   [main.assertion.2]  line 11  loop invariant inductive step
    UNKNOWN  [main.assertion.3]  line 16  assertion s == 3 (loop invariant too
             weak to prove this claim: the counterexample is against the havoc
             abstraction, not a reachable state of the program)
  
  ** 0 of 3 properties failed, 2 passed, 1 unknown
  WARNING: every violated claim lies downstream of a loop invariant havoc, so
  its counterexample is against the abstraction rather than the program;
  strengthen the invariant to decide the claim
  
  VERIFICATION UNKNOWN

  Strengthen the invariant until it entails the property. This mode cannot report a bug after an annotated loop; plain BMC and --k-induction, whose base case keeps the original loop, remain the modes that refute. What keeps reporting FAILED is a claim ahead of every havoc, the invariant’s own inductive step and its assigns-compliance check, and a loop the schema declined. An outermost loop’s base case does too, since no havoc precedes it; an inner loop’s base case sits inside the outer body, downstream of the outer havoc, so it is downgraded with everything else there.

• The schema declines a loop it cannot havoc soundly instead of claiming a proof: a body (or a callee) that writes only through a pointer, where the guard reads nothing the havoc covers, leaves nothing for the modified-variable analysis to record. Such a loop is left to the unwinder, with a warning — loop invariant at <location> not checked beyond its base case: the loop writes through a pointer the havoc cannot cover — and its base case is still checked, since that runs from the concrete pre-loop state.

• Cutting the loop establishes partial correctness only: termination is not proved. Use --termination separately if you need it.

Example: Property Follows From the Invariant Alone

x == y is exactly what the assertion needs, so the inductive step closes at k = 2 and the loop bound is irrelevant — this verifies as quickly at 100000 as at 10.

#include <assert.h>

int main(void) {
    unsigned int x = 0;
    unsigned int y = 0;

    __ESBMC_loop_invariant(x == y);
    while (x < 100000) {
        x++;
        y++;
    }

    assert(x == y);
    return 0;
}

esbmc file.c --loop-invariant
# VERIFICATION SUCCESSFUL — Solution found by the inductive step (k = 2)

Example: Property Needs the Exit Condition

Here sum == 10000 follows only from sum == i * 10 and i == 1000, and the latter needs !(i < 1000) at exit. This is the case that requires --loop-invariant-check; under --loop-invariant it reports VERIFICATION UNKNOWN because the bound exceeds the k-induction step limit.

#include <assert.h>

int main(void) {
    unsigned int i = 0;
    unsigned int sum = 0;

    __ESBMC_loop_invariant(i <= 1000 && sum == i * 10);
    while (i < 1000) {
        sum += 10;
        i++;
    }

    assert(sum == 10000);
    return 0;
}

esbmc file.c --loop-invariant-check
# VERIFICATION SUCCESSFUL

The same shape appears whenever a loop fills an array and the postcondition quantifies over it, which is why array contracts under --enforce-contract normally want --loop-invariant-check:

__ESBMC_ensures(__ESBMC_forall(&i, !(i < N) || (a->e[i] >= 0 && a->e[i] < Q)));

__ESBMC_loop_invariant(i <= N && __ESBMC_forall(&j, !(j < i) ||
                       (a->e[j] >= 0 && a->e[j] < Q)));
for (i = 0; i < N; i++)
  a->e[i] = reduce(a->e[i]);

With --loop-invariant-check this discharges in a fraction of a second for any N, and --unwind only has to cover the rest of the function rather than the loop.

Companion Options

The following options can be combined with the k-induction proof rule to produce or strengthen inductive invariants:

• --interval-analysis — Enable interval analysis for integer variables and inject assume statements into the program.
• --add-symex-value-sets — Enable value-set analysis for pointers and inject assume statements.
• --loop-invariant — Use user-provided loop invariants with the combined k-induction mode (described above).

Known Limitations

Nested Loop Support: The current implementation does not correctly handle nested loops with multiple invariants. State management between inner and outer loops requires further refinement.

Manual Invariant Specification: Users must manually specify correct loop invariants. ESBMC will not infer or validate invariants before verification. An incorrect invariant will lead to a failed base-case assertion in --loop-invariant mode, or an undecided claim in --loop-invariant-check mode.

Note: --loop-invariant-check havocs every loop-modified variable, so an invariant that does not constrain them enough leaves the claims after the loop undecided (commonly an integer-overflow report), and they are reported UNKNOWN. --loop-invariant does not have this failure mode. If you hit it, either strengthen the invariant or, when the property follows from the invariant alone, switch to --loop-invariant.

--k-induction-parallel still reports a downgraded claim as FAILED. The downgrade is recorded in the parallel driver but the verdict does not follow it back across the fork (#7516).

Mode Summary

Programs without loop invariant annotations continue to use the standard k-induction unwinding approach under either flag.

Loop Frame Rule (--loop-frame-rule)

A loop invariant says what stays true across iterations. The loop frame rule adds the complementary claim: which variables the loop is allowed to change. Variables not listed in __ESBMC_loop_assigns are guaranteed to be untouched — and ESBMC checks this.

int main(void) {
    int i = 0;
    int j = 42;

    __ESBMC_loop_invariant(i >= 0 && i <= 10);
    __ESBMC_loop_assigns(i);
    while (i < 10)
        i++;

    /* j was not listed in loop_assigns — ESBMC can prove it is still 42 */
    __ESBMC_assert(j == 42, "j unchanged");
    return 0;
}

Run with:

esbmc file.c --loop-invariant-check --loop-frame-rule

Without --loop-frame-rule, the havoc step makes every loop-modified variable nondeterministic, so the assertion on j would fail despite j never being touched. With the flag, ESBMC snapshots all variables not in __ESBMC_loop_assigns before the havoc and assumes they are unchanged afterward.

Both macros must be placed before the loop, as statements ending with ;. __ESBMC_loop_assigns supports up to five targets; use __ESBMC_loop_assigns() with no arguments to declare that the loop modifies nothing.

--loop-frame-rule requires --loop-invariant-check. It does not work with --loop-invariant (the combined k-induction mode).