[CatarinaGamboa]

Problem

When a method reads a field, Found shows a row for it under its internal name, and the row says only true. Issue reproducer (ArrayList.size() refined _ == size(this) && _ >= 0, Random.nextInt(bound) refined bound > 0):

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

In the IDE the first row wraps over several lines, above the row that matters. The message and the later row also write the field as items, so it reads like the local it was copied into.

Cause

1. VCBinderSimplification dropped a true binder only when no later row mentioned its variable. Here size(this#shop.Basket.items) mentions it. Every field, parameter, call result or local that is only passed along keeps its true row this way. The ∀getUndoManager⁸⁵⁶ true and ∀#fresh… true rows of Simplify trues when not used #375 come from the same rule.
2. VariableFormatter.format left this#<package>.<Class>.<field> unchanged. The binder, the counterexample and the extension's context and translation-table keys therefore showed the internal name, while ExpressionNameResolver cut it down to the bare items inside expressions.

Fix

Which true rows stay

A binder refined only by true states no fact. It stays in Found only when the error needs it:

• Linked to Expected. Some fact of the chain constrains the binder's value and is linked to Expected, meaning it shares a term with Expected directly or through other linked facts.
  • Terms are variables and ghost or state applications such as size(x).
  • Facts are the rows' conjuncts. A negated disjunction is split first: !(p || q) becomes !p and !q, so one combined guard does not link everything.
  • A variable of an object type that a fact names only as a ghost argument (x in b == size(x)) is not constrained by that fact. Its row would say nothing, so it goes. A primitive argument (k in y == f(k)) has a value of its own and is kept.
• Expected constrains its value, in a refinement error only. The counterexample then shows that value; filterCounterexample lists only binders. A state error has no counterexample, so there this alone keeps nothing.

The rule depends only on the chain and Expected, not on Z3's model, and it works the same way for both error kinds.

A kept true binder that comes after a row using its variable is moved to just before that row. This is a separate Binder step.

Examples:

Case	Rows (after)
issue reproducer	∀bound⁶ bound⁶ == size(this.items) && bound⁶ >= 0 (field only inside size(...))
if (port < 0) return; positive(t);	∀#fresh !(port < 0), ∀t true: port dropped (unlinked guard), t kept (Expected, counterexample t == 0)
if (p || q) return; positive(t);	∀#fresh !(p || q), ∀t true: p and q dropped
int y = x + 1 refined _ > 0	∀x true, ∀y y == x + 1: x kept, linked through y
ErrorStateHintPathDependent (state)	∀ready true, ∀f ready ? open(f) : created(f): ready kept
state errors whose Found is otherwise true	unchanged from main: no ∀it true / ∀this true row is added
for (int i = start; i < served; i++) positive(i);	∀Basket.served true, ∀i true, ∀#fresh i < Basket.served: i now before its first use

The linking is VCSimplificationUtils.linkedConjuncts(conjuncts, termsOf, seed). It does what linkedTerms in RefinementError does on #460 (branch fix/counterexample-expected-vars, issue #453): the same closure over shared terms, with the term function passed in. Once both are merged, linkedTerms can call this helper with its termsOf, and splitConjuncts can replace getConjuncts there, so the counterexample and the rows are linked in the same way. I didn't touch filterCounterexample.

Simplification history (the VS Code arrows)

Dropping a true row is an ordinary simplification step of the Binder pass, one binder per step. It goes into VCSimplificationResult's origin chain, which the extension's server sends whole (VCSimplificationResultDTO.origin). The panel steps back through that chain, and its last step is the untouched Original with every binder.

What the panel shows for the issue reproducer:

Step	main (2 steps)	this branch (3 steps)
1 Original	∀this#shop.Basket.items true ∀items⁵ items⁵ == this#shop.Basket.items ∀bound⁶ bound⁶ == size(items⁵) && bound⁶ >= 0	∀this.items true ∀items⁵ items⁵ == this.items ∀bound⁶ bound⁶ == size(items⁵) && bound⁶ >= 0
2 after Substitution	(Simplified) ∀this#shop.Basket.items true ∀bound⁶ bound⁶ == size(items) && bound⁶ >= 0	∀this.items true ∀bound⁶ bound⁶ == size(this.items) && bound⁶ >= 0
3 after Binder		(Simplified) ∀bound⁶ bound⁶ == size(this.items) && bound⁶ >= 0

The field display name is applied at every step, including Original, because the server formats every step with VariableFormatter.format. The internal names are untouched in the history itself. TestFoundBinders.steppingBackReachesTheOriginalWithTheDroppedRow checks that the original's binders are this#testSuite.classes.found_true_binders_error.Basket.items, #items_…, #bound_…. Showing the Original raw would be a one-line change in VCImplicationDTO (skip format for the oldest step), but I left that for the PM to decide.

Source-like field names

this#pkg.Class.field is written this.field in the message, the Found rows, the counterexample and the extension's context and translation table. This holds for both this.x and bare x. A static field is written Class.field. Instance counters stay (this.interrupts¹¹³), nested classes and long package names reduce the same way, and the internal SMT name is unchanged.

Static-ness is not in the name, so Utils.qualifyFieldName records static fields as it builds their names, and CommandLineLauncher.launch clears the record at the start of each run. Every error comes from code verified in that run, which also built the names of the fields it shows, so the record is complete for that run's errors. Verifying a static total, then an instance total of the same class, then the static one again in one JVM shows C.total, this.total, C.total. There is no incremental verification that skips classes. If one is added, the record would need to be filled from the field declarations instead.

I removed the earlier class-based disambiguation (Basket.this.count). Real code could not reach it, it was not valid Java for inherited fields, and it was not applied to binder rows or translation-table keys. Two different fields with the same simple name in one expression (a shadowed field) now both read this.x.

Writes to another object's field (display only)

This PR does not change what the verifier accepts or rejects for any write. A write to another object's field (other.level = …, other.level++, other.level--, other.level += …) is still checked and tracked exactly as on main, against the current object's field variable.

Only its label changes. When TypeChecker.checkVariableRefinements creates the new instance for a write that Utils.accessesTrackedField says is not to the current object, it records the receiver's variable name for that instance in VariableFormatter (a bare field name when the receiver is not a variable). The instance is then written other.level¹ instead of this.level¹:

main:   level¹ == -1 is not a subtype of level¹ >= 0
now:    other.level¹ == -1 is not a subtype of other.level¹ >= 0

Because tracking is unchanged, a decrement shows what the verifier actually uses as the old value: other.level⁹ == this.level⁸ - 1. Writes through another object leak into this.level, and aliasing with this is not handled. Both are left for their own issue.

Parity with main, checked on the reviewers' reproducers and ErrorOtherObjectFieldWrite.java:

• other.level++, other.level += 1 and other.level = other.level + 1 verify.
• other.level-- and other.level = -1 are reported.
• The write through W other = this and maybeSelf(this) are reported.
• The other.level = 5; int k = this.level (_ == 5) case verifies as on main.

#375

This covers part of #375, not all of it. The true rows go, and in the JabRef EditAction exercise all four are removed. The path conditions over now-undeclared fresh variables (∀#fresh¹²² !#fresh¹²¹) are not true rows and stay; they also tie in with #373. #375 stays open.

Before / after (main vs this branch, every error)

I ran the harness that dumps what the IDE gets (message, rows, counterexample, translation-table keys) over 321 test-suite errors and 117 errors from the 98 study exercises, with main and this branch on identical inputs:

• The same errors are reported at the same lines on both sides (the harness requires it), so nothing that main accepts or rejects changes.
• 58 test-suite errors and 57 exercise errors differ in what they show.
• The differences are renames (this#… to this.x or Class.x), dropped true rows, the Binder reordering, and in refinement errors a kept true row for an Expected variable. In those refinement errors main showed only true; now the variable's counterexample value also shows, e.g. port == 65536.
• true rows: 110 → 87 (test suite), 78 → 46 (exercises). Raw this# names: 30 → 0 and 72 → 0.
• No state error gains a true row.
• Instance numbers do not move: 0 of the 438 messages change their superscripts. I could not reproduce the transactionCommitted²⁷→²⁸ shift (A1_50 shows ²⁸ on both). I think it came from different inputs between the two runs.

Several fields (pickAny)

before: ∀this#testSuite.classes.found_true_binders_error.Basket.items³⁷   true
        ∀first³⁸   first³⁸ == size(items³⁷) && first³⁸ >= 0
        ∀this#testSuite.classes.found_true_binders_error.Basket.extras⁴¹   true
        ∀second⁴²  second⁴² == size(extras⁴¹) && second⁴² >= 0
        ∀bound⁴⁵   bound⁴⁵ == first³⁸ + second⁴²
after:  ∀first³⁸   first³⁸ == size(this.items³⁷) && first³⁸ >= 0
        ∀second⁴²  second⁴² == size(this.extras⁴¹) && second⁴² >= 0
        ∀bound⁴⁵   bound⁴⁵ == first³⁸ + second⁴²

Static field, linked to Expected (serve)

before: count⁵⁴ == served + 1 is not a subtype of count⁵⁴ > 0
        ∀this#testSuite.classes.found_true_binders_error.Basket.served   true
        ∀count⁵⁴   count⁵⁴ == served + 1
after:  count⁵⁴ == Basket.served + 1 is not a subtype of count⁵⁴ > 0
        ∀Basket.served   true
        ∀count⁵⁴   count⁵⁴ == Basket.served + 1
        Counterexample: Basket.served == -1 && count⁵⁴ == 0

Field holding a state kept, unrelated true parameter dropped (classes/found_field_state_error, after Jpcsp's IntrManager)

before: ∀intrNumber   true
        ∀#fresh¹⁶     !(intrNumber < 0 || intrNumber >= 67)
        ∀this#testSuite.classes.found_field_state_error.InterruptManager.interrupts¹³   empty(interrupts¹³)
after:  ∀#fresh¹⁶     !(intrNumber < 0 || intrNumber >= 67)
        ∀this.interrupts¹³   empty(this.interrupts¹³)

Tests

• TestFoundBinders (19 tests) on the fixtures classes/found_true_binders_error, classes/found_field_state_error, ErrorStateHintPathDependent.java and the new ErrorOtherObjectFieldWrite.java:
  • dropped: the reproducer's field row; a true parameter, call result and local; several fields; port behind an unrelated guard; p/q behind one combined guard.
  • kept: x linked through y == x + 1; an Expected variable in a refinement error; ready in the path-dependent state error; the field row holding empty(...).
  • row order for a loop variable.
  • names: static Basket.served; this.amount and bare amount written alike; an inner-class field; other.level for writes and decrements on another object, and this.level for an own write.
  • parity with main for writes: other.level++ and other.level += 1 verify; other.level-- and the write through an alias of this are reported.
  • the original the panel steps back to keeps the dropped row and the raw binder names, and the history includes a Binder step.
• VCBinderSimplificationTest (13 new, including a primitive ghost argument that is kept):
  • linked through one or several rows;
  • an unlinked guard;
  • a split negated disjunction;
  • an Expected binder in refinement vs state errors;
  • linking through a ghost while keeping only value variables;
  • an object named only inside a ghost;
  • moving a kept binder before its first use;
  • the NeededVariables factories.
• VCSimplificationUtilsTest (4): splitting conjuncts and negated disjunctions; transitive linking.
• VariableFormatterTest (6 new) and ExpressionNameResolverTest (2 new): instance, static, nested, long-package and other-object field names; clearing the static record between runs; a field next to a local of the same name; a field inside a ghost argument.

Without the fix (main sources, the new tests kept), TestFoundBinders fails 15 of 19 and ExpressionNameResolverTest fails 2 of 5. The unit tests on the new API do not compile on main.

mvn test (verifier): 583 tests, 0 failures (main: 534).

Changed existing expectations

• VCBinderSimplificationTest.keepsTrueBinderWhenVariableIsUsedDownstream became removesTrueBinderUsedDownstreamWhenNothingNeedsIt: with nothing to link to, the binder goes. That is the rule change itself.
• VCBinderSimplificationTest.skipsInapplicableTrueBinderAndSimplifiesLaterBinder now makes x an Expected variable, so its binder is still the inapplicable one the test is about. The expected steps are unchanged.
• VCTestUtils.parseImplication splits a binder at the first . after the :, so binder names can contain dots.

No // Expect: fixture, TestCounterexamples or TestErrorCategories expectation changed.

Not in this PR

• Raw names in the Original step (above).
• random.nextInt(items.size() + extras.size()) fails on main with Sort mismatch … supplied sort is …Basket, a separate translation bug. The fixture uses two locals instead.
• The client's hover (getOriginalVariableName) strips only this#, so it does not match fields, before or after this change. Stripping a leading this. there would be a small follow-up in vscode-liquidjava.

Fixes #457

🤖 Generated with Claude Code

[CatarinaGamboa]

Removing the true's is a simplification right? in vscode, if we use the arrows to go back we can see the addition of the true's correct? We also want to be able to show the initial version without any simplifications when the user goes back enough times

[CatarinaGamboa]

[Codex review] The new field-name disambiguation still collides when different declaring classes have the same simple name. For example, register static fields this#alpha.Basket.served and this#beta.Basket.served: VariableFormatter.formatWithOwner renders both as Basket.served (I confirmed this on this PR head). ExpressionNameResolver detects that their normal displays collide but then uses formatWithOwner, so a diagnostic containing both fields remains ambiguous. The same applies to two instance fields, which both become Basket.this.served. Please use enough of the qualified owner name to distinguish them when the simple owner names collide, and add tests with two packages declaring Basket. The focused formatter and binder tests passed.

[CatarinaGamboa]

[Claude] Yes, removing the true rows is a simplification. Each one is dropped by its own Binder step in the simplification history, which the extension's server sends whole (VCSimplificationResultDTO.origin). Going back with the arrows brings the rows back one step at a time, and the oldest step is the untouched Original with every binder.

For the issue reproducer the panel now shows 3 steps instead of 2:

1. Original: ∀this.items true, ∀items⁵ items⁵ == this.items, ∀bound⁶ …
2. Substitution: ∀this.items true, ∀bound⁶ bound⁶ == size(this.items) && bound⁶ >= 0
3. Simplified (Binder): ∀bound⁶ bound⁶ == size(this.items) && bound⁶ >= 0

The source-like field names (this.items) are applied at every step, including Original. The server formats every step with VariableFormatter.format. The internal names in the history itself are unchanged (this#…Basket.items). If you want the Original step shown raw, that is a one-line change in the extension's VCImplicationDTO. I haven't made it; tell me if you'd like it.

In 0b45301. Test: TestFoundBinders.steppingBackReachesTheOriginalWithTheDroppedRow checks that the original keeps the dropped row and the raw binder names, and that the history has a Binder step. The table in the PR description compares the steps on main and on this branch.

[CatarinaGamboa]

[Claude] I removed the disambiguation instead of extending it, following an earlier review. formatWithOwner and the Basket.this.count form are gone in 0b45301. The same-name case couldn't be reached from real code. Basket.this.x isn't valid Java for an inherited field. And the binder rows and translation-table keys never used that form, so the rows and the message disagreed.

Every field is now written one way everywhere: this.x, Class.x for a static field, or other.x for a write to another object's field. With this#alpha.Basket.served and this#beta.Basket.served in one expression, both read Basket.served. The same goes for a field and the field it shadows. That is listed as a limitation in the PR description. Tests: VariableFormatterTest and ExpressionNameResolverTest (the owner-disambiguation tests were removed with the feature).

[CatarinaGamboa]

[Codex re-review] The update correctly distinguishes writes such as other.level = -1 from writes to this.level, and makes the formatter print other.level for the other-object field. The true-binder rule now follows facts linked to Expected rather than keeping every referenced true binder. The owner-name collision I raised remains an acknowledged display limitation: alpha.Basket.served and beta.Basket.served can still both render as Basket.served. If that output remains acceptable, please keep it documented; otherwise qualify owners only when their displayed names collide. The PR CI is green.

[CatarinaGamboa]

[Claude] Writes to another object's field are back to main's behaviour; the change for them is now display-only (0c17f78). RefinementTypeChecker, OperationsChecker and AuxStateHandler are identical to the branch base again. The only addition is in TypeChecker.checkVariableRefinements: when an untracked write creates a new instance, it records the receiver's name for that instance in VariableFormatter. The instance is then shown as other.level¹ instead of this.level¹. The verifier still checks and tracks the write as on main.

Results match main:

• other.level++, other.level += 1 and other.level = other.level + 1 verify.
• other.level-- and other.level = -1 are reported.
• The write through W other = this and maybeSelf(this) are reported.
• The other.level = 5 leak verifies, as on main.

The write soundness issues (the leak into this.level, aliasing with this) are left for their own issue, and the PR body no longer claims them.

Also: a true binder that is a primitive ghost argument (k in y == f(k)) is now kept. Only object-typed ghost arguments are skipped.

Tests: TestFoundBinders.writesToAnotherObjectsFieldAreCheckedAsOnMain, TestFoundBinders.writeToAnotherObjectsFieldIsWrittenWithThatObject, VCBinderSimplificationTest.keepsPrimitiveTrueBinderThatIsTheArgumentOfAGhost, VariableFormatterTest.writesAnInstanceCreatedByAWriteThroughAnotherObjectWithThatObject. Verifier mvn test: 583 tests, 0 failures. Comparing main and this branch over 321 test-suite errors and 117 exercise errors gives the same errors at the same lines; 58 and 57 of them differ only in what they show.

[CatarinaGamboa]

[Claude] Rebased onto main after #460 merged. One assertion changed: staticFieldIsWrittenWithItsClass now expects count == 0 && Basket.served == -1, because #460 lists Expected's values first. The full suite passes locally on the rebased branch.

[CatarinaGamboa]

[Codex re-review] No new issues found on the updated head; CI is green.