[CatarinaGamboa]

Problem

Two failures in how visitCtIf joins the branches, both from the guard it puts in the joined instances.

1. A reference comparison loses the then-branch state (missed error).

Door d = new Door();          // open
if (other == d) {
    d.close();
}
d.close();                    // passes, but d may already be closed

The guard was the condition with variable names and with their instances (other == d && other == #d_8). After the if, a variable's name stands for its latest instance, so d in the guard became the joined instance: the then-case required the joined d to be the same object as #d_8, which is open, so the closed branch was impossible and the error was missed.

2. A call result in a nested if's condition leaves scope (internal error).

Door d = new Door();
if (b) {
    if (current() == d) { ... }
}
d.close();   // Not Found Error: Variable '#fresh_11' could not be found

The fresh variable for current() lives in the outer then-block, but the inner join's guard (in d's joined instance) still uses it after that block ends.

Fix

• The join uses a guard that names only the instances the condition read (lastExpRefs). The branch assumptions are unchanged.
• The fresh values in that guard (and the fresh values their refinements use) are kept in the context as instance variables, so they outlive the block that created them.

With the fix, case 1 reports found open(d⁸) && (d⁸ == other ? closed(d¹³) : open(d¹³)) but expected open(d¹³).

Tests

• CorrectNestedIfCallComparison: case 2, correct code. It failed before this change.
• ErrorNestedIfCallComparison: case 2 with a close in the inner branch, then another close: reported.
• ErrorIfReferenceComparison: case 1: reported. It passed before this change.
• mvn test: 415 tests, 0 failures.

Found on a real fixed bug (a game engine's window switching display modes, which compares the full-screen window with its frame inside an outer if). We also checked 53 exercises built from real OSS bugs on main (e0a6c81) and with this change: the results are identical except for one exercise whose fix crashed with Variable 'length' could not be found and now verifies.

🤖 Generated with Claude Code

[CatarinaGamboa]

This still leaves a soundness gap when a condition reads a variable that has no last instance (for example, a method parameter). substituteAllVariablesForLastInstance leaves b as a name, so a later assignment changes the meaning of the already-joined guard:

// Door() establishes open(this); close() requires open(this) and establishes closed(this).
void closeTwice(boolean b) {
    Door d = new Door();
    if (b == true) d.close();
    b = false;
    d.close(); // should be a State Refinement Error
}

I ran this on the PR head; LiquidJava says Correct! Passed Verification. The join uses the current b == true (false), discarding the path where d was closed. Could we snapshot condition operands even when they have no existing instance, and add a regression for mutation after the if? This appears to be an existing weakness that the new joinGuard does not cover.

[CatarinaGamboa]

The retention walk stops at a value already in ctxInstanceVars, even though that value's refinement can refer to a block-local #fresh value. This leaves the nested-if scope failure unresolved for a refined boolean call whose argument is an expression:

@Refinement("_ == 1") static int one() { return 1; }
@Refinement("_ == (n > 0)") static boolean positive(int n) { return n > 0; }
void check(boolean b) {
    Door d = new Door(); // initially open
    if (b) {
        if (positive(one() + 1)) d.close();
    }
    d.close(); // should be a State Refinement Error
}

On this head the second close() instead reports Not Found Error: Variable '#fresh_12' could not be found. Here the joined guard names the synthetic condition value, which is already an instance; the chain through the call's argument refinement to #fresh_12 is never traversed. Please test transitive dependencies of nested conditions, including values already retained as instances.

More broadly, this fix promotes block-local values into the method-wide instance list. Could we document the intended lifetime/scope invariant for values captured by a join and check that this approach fits it? Issue #406 describes the same kind of out-of-scope refinement dependency across try/finally; a general treatment may be safer than handling only names with the #fresh prefix here.