while loop condition is not assumed inside the loop body #306

Description

The condition of a while loop is not used as a fact inside its body, unlike the condition of an if. A value that the loop condition proves to be in range is reported as possibly out of range.

Minimal reproducer

import liquidjava.specification.Refinement;

public class Repro {
    @Refinement("_ >= -1")
    static int next() { return -1; }

    static void use(@Refinement("_ > 0") int n) {}

    static void drain() {
        int size = next();
        while (size > 0) {
            use(size);              // safe: the loop condition guarantees size > 0
            size = next();
        }
    }
}

Expected

Correct! Passed Verification.: inside the body size > 0 holds (on entry and after each re-assignment, since the condition is re-checked).

Actual

Running LiquidJava on: <repro dir>

Refinement Error: size³ >= -1 is not a subtype of size³ > 0
10 |         int size = next();
11 |         while (size > 0) {
12 |             use(size);              // safe: the loop condition guarantees size > 0
   |             ^^^^^^^^^^
13 |             size = next();
14 |         }
 --> Counterexample: size³ == -1

<repro dir>/Repro.java:12

--> Refinement declared here:

Reproduced on main at 8816186 (liquidjava-verifier 0.0.35), and on 0.0.33.

Context

Found while turning real open-source Java code into study examples for the error-message study: real code hits this constantly, so the examples have to be rewritten around it or cannot be verified. The usual read loop n = in.read(buf); while (n > 0) { out.write(buf, 0, n); n = in.read(buf); } fails this way. At least assuming the condition, as for if, would cover it.