"for i = A to B do invariant I ... done" now requires (A <= B+1)
and I(A) unconditionally, and has a single outcome under I(B+1).

To restore the old behaviour (where the loop code is handled
under (A <= B) and there is a separate outcome under (A > B)),
put the label "vc:liberal_for" over the loop expression.

We believe that the (A <= B+1) condition is likely, and asserting
it by default allows us to avoid the second outbound branch.