[CatarinaGamboa]

Closes #375.

Problem

#459 dropped the true binders the error does not need. When the dropped binder was the last one of Found, VCBinderSimplification.removeBinder replaced it with a bare true row, so Found still ended in true after the path conditions. That is the case of the issue's screenshot: wParam comes from writer.getDefaultWriteParam(), nothing is known about its state, and its ∀wParam true row turned into a bare true that reads as if baseline || extended were true.

Change

In VCBinderSimplification, a suffix that simplifies to just true is left out of the row above it (withNext/isPlainTrue). This covers a dropped last binder and a collapsed false binder. It happens in the same Binder step, so the panel's history gets no extra step.

• A Found that simplifies away entirely still shows a lone true (found true but expected …). Nothing is known, and an empty Found would hide that.
• Rows with content, path conditions and binders the error needs are unchanged. The message's found … text doesn't change either, because P && true was already printed as P.

Before / after

Study exercise A1_01 (dcm4che SlideRecoder, line 131), the issue's screenshot:

before (main):                          after:
∀#fresh²⁹⁷   baseline²⁹³ || extended²⁹⁴  ∀#fresh²⁹⁷   baseline²⁹³ || extended²⁹⁴
true

Other cases (checked while developing; the unit tests below cover the rule):

Case	Before (main)	After
no path condition	true	true (unchanged)
if (baseline || extended)	∀#fresh baseline || extended, true	∀#fresh baseline || extended
nested if (lossless) if (!extended)	∀#fresh #fresh == lossless && #fresh, ∀#fresh !extended, true	same rows, no true
known state in a branch	∀#fresh …, ∀wParam startCompression(wParam)	unchanged

Study exercise A1_56 (JabRef EditAction, the issue comment) already had no true rows on main after #459. It is unchanged:

∀#fresh¹¹²        !#fresh¹¹¹
∀#fresh¹²⁶        !(#fresh¹²⁴ || #fresh¹²⁵)
∀undoManager¹³¹   undoManager¹³¹ == getUndoManager¹²⁹

Follow-up (not in this PR)

The guard rows above (∀#fresh¹¹² !#fresh¹¹¹, ∀#fresh¹²⁶ !(…)) say nothing about Expected, and they use fresh variables whose binders were dropped. In A1_01, the one row left (baseline || extended) also says nothing about wParam. Whether to drop path conditions unrelated to Expected is pending the PM's decision. The #fresh names are #373.

Tests

• VCBinderSimplificationTest: 3 new tests: a last true binder after a path condition, after nested conditions, and a collapsed false binder after a row. trueBinderWithoutSuffixBecomesPlainTrue (lone true) still holds.
• Without the fix, all three new unit tests end in true.
• mvn test (verifier): 684 tests, 0 failures. No existing expectation changed.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

(Codex v0.164.0, codex exec review, on commit 7a656f2. Its shell sandbox cannot start on this machine (bwrap: loopback: Failed RTM_NEWADDR), so it was given the PR description, the diff against origin/main and the full changed and related files on stdin.)

The change removes the trailing true row when binder simplification produces it, while preserving a lone true result. I found no concrete correctness bug or blocking test gap in the supplied diff.

[CatarinaGamboa]

Codex review, round 2

(On commit 6c948cb, same setup as round 1. Between the rounds I changed one thing myself: the code comment P => true -> P read as an implication, where P => true is just true. It now says that Found reads its rows as a conjunction (P && true -> P). Full suite: 689 tests, 0 failures.)

The change removes trailing plain-true rows while preserving a lone true result, and the supplied tests cover the reported cases. I found no concrete correctness bug in the provided diff.

Neither round found anything, so there is nothing to fix or decline, and the review loop ends here.