GeezerVison

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