Impact: a field read in the method shows up in Found as its internal name, this#<package>.<Class>.<field>, and only as true. In the IDE panel this row wraps over several lines, comes before the useful one, and the name isn't the one used in the code or in the message.

Minimal reproducer (ArrayList.size() refined _ >= 0 and Random.nextInt(bound) refined bound > 0, in external specs)

package shop;

public class Basket {
    private final ArrayList<String> items;
    private final Random random = new Random();

    Basket(ArrayList<String> items) {
        this.items = items;
    }

    String pick() {
        ArrayList<String> items = this.items;
        return items.get(random.nextInt(items.size()));
    }
}

Actual (main @ 19991d3). Message: bound³⁴ == size(items) && bound³⁴ >= 0 is not a subtype of bound³⁴ > 0. Found, as sent to the IDE:

∀this#shop.Basket.items   true →
∀bound³⁴                  bound³⁴ == size(items) && bound³⁴ >= 0

Expected: no row for a binder that is only true and that no other row needs (see #375), or at least the source name: this.items.

Real-world scenario. Two exercises for the error-message study show it:

• chaos-http-proxy's RandomFailureSupplier shows ∀this#x_e_oss_a2_10_randomfailuresupplier.E_OSS_A2_10_RandomFailureSupplier.failures above the actual cause.
• Jpcsp's IntrManager shows ∀this#x_e_oss_a1_17_interruptmanager.E_OSS_A1_17_InterruptManager.interrupts⁴⁷⁵, which is the row that holds the state (empty(...)).

Related: #375, #373, #132.

In VS Code (chaos-http-proxy study exercise, verifier main @ 19991d3, extension main @ 80bed18). The field row wraps over five lines above the useful one: