GeezerVison

Problem

The branches of a conditional expression were checked without knowing which way its condition went:

boolean canUndo = um.canUndo();
return canUndo ? um.getUndoPresentationName() : "Undo";

State Refinement Error: found canUndo ? end(um) : true but expected canEdit(um) || end(um)

The same guard written as an if passes. visitCtConditional scanned the condition and both branches with no path condition, then only built the ITE for the expression's value.

Fix

• visitCtConditional scans the condition, then each branch with the condition (then) or its negation (else) as a path condition, removed after the branch.
• The encoding is the loop condition's (assumeLoopCondition), now assumeCondition(condition, holds); loops call it with true. Conditions with side effects still assume nothing.

Tests

• CorrectTernaryConditionInBranch: full ? box.peek() : 0 where peek needs full(this) and full is box.isFull(). It failed before this change.
• ErrorTernaryConditionInBranch: full ? 0 : box.peek(): still reported.
• mvn test: 429 tests, 0 failures.

Found on a real fixed bug (JabRef's CountingUndoManager, which labels its undo and redo events with canUndo ? getUndoPresentationName() : ...). We also checked 53 exercises built from real OSS bugs on main (e0a6c81) and with this change: the results are identical.

🤖 Generated with Claude Code