source: CIVL/mods/dev.civl.com/examples/loop_invariants/dev/plan@ cb4d4f4

loop init;
assert( invari );
if (cond)
  while(true) {
    assume_push(cond && invari);
    body;
    increment;
    assert
    havoc
    if (!cond) break;
    assume_pop();
  }