[SwayamInSync]

A loop that never runs still havocked every variable it assigns, so its function was refuted with a counterexample no execution produces. do { ... } while (0), the usual way to write a statement-like macro, is such a loop:

#define SWAP_INT(a, b) do { int t_ = (a); (a) = (b); (b) = t_; } while (0)

int swapped_diff(int x, int y)
  cppverify::pre(0 <= x && x <= 100 && 0 <= y && y <= 100)
  cppverify::post(cppverify::result == y - x)
{
  int a = x;
  int b = y;
  SWAP_INT(a, b);
  return a - b;
}

On main this fails an overflow check with a = -2, and int r = x; while (false) { r = r + 1; } return r; fails post(result == x). Without a decreases clause either would also have been decreases.missing.

A loop whose condition is a constant false (an integer constant expression, such as while (false) and the macro's while (0)) now keeps every variable it would change, and needs no measure, since it never repeats. Its invariants are still checked on entry. Any other loop is unchanged. Keeping the entry state wherever the condition is false on entry would be exact too, but the extra case split cost the proof of encode_uleb128 in llvm_uleb128.cpp (solver.timeout), so such a loop stays described by its invariant.

old_loop_invariant_definedness_fail.cpp failed only through this havoc. Contract arithmetic is mathematical, so its old(value + 1) cannot overflow; the failures it saw were spurious postcondition counterexamples. Its first two cases now convert explicitly, old((int)(value + 1)), the overflow they meant, and the test checks the obligation kind.

Testing: suite/loop_zero_iterations.cpp fails on main, and fails if either change is removed (the Layer 2 check sees the kept values). Verify suite: 398 passed, 1 unsupported, with the repaired test. A verdict differential against main over the 405 Verify sources changes only the two cases above (2959 s on main, 2895 s here).