GeezerVison

## Problem

When Found says nothing about the variable that Expected constrains, the
counterexample leaves that variable out. It shows values for unrelated
path conditions instead:

```
Refinement Error: !(port < 0 || port > 65535) is not a subtype of timeout >= 0
 --> Counterexample: port == 0
```

The value that breaks the call (`timeout == -1`) is in the SMT model,
but it gets filtered out. In the OpenNMS study exercise the panel shows
`#fresh³¹⁶ == false && port³¹³ == 0`, which points the reader at the
port guard.

## Cause

`RefinementError.filterCounterexample` kept only assignments to the
**binders of the simplified Found**. That rule is wrong in three ways:

1. **It drops what Expected constrains.** A variable Found only knows as
`true` loses its binder during simplification, so its value goes too
(`timeout`, and also `size(bag)` for ghosts).
2. **It drops variables Found does mention.** A variable whose binder
was simplified away can still appear in a path condition.
3. **It keeps noise.** It keeps any surviving binder, even one nothing
displayed mentions (a generated path binder). It keeps path conditions
unrelated to Expected. It keeps raw Z3 array values (`l == ((as const
(Array Int Int)) 4)`).

## Fix

The counterexample exists to show values that make Expected false under
Found.

**What is kept**

- **The terms of Expected.** These are its variables and its ghost
applications over variables (`size(bag)`, `length(a)`), named as the SMT
model names them.
- **The terms of every Found fact linked to them**, directly or through
other facts. A fact is a conjunct of Found. Negated disjunctions are
split (`!(a || b)` gives `!a` and `!b`), and double negations are
dropped. So one combined guard `!(port < 0 || … || timeout > 60000)`
links only `timeout > 60000` to `timeout`, not every variable in the
guard. A fact that shares no term with Expected only constrains values
that cannot affect it, so it is left out.
- **Not values Found already states.** An `x == v` fact is compared
structurally. Enum constants match the model's value (`Format.JPG` in
Found, `JPG` in the model), and so do ghost applications with several
arguments.
- **Nothing when Found fixes every value Expected depends on.** There is
no fallback to other terms: `int value = 0; if (port > 0) take(value);`
against `_ > 1` shows no counterexample rather than `port == 1`. This is
the same rule that already gives literal arguments no counterexample
(`ErrorLiteralZero`). A path condition is shown only when it is linked
to Expected, e.g. `return port + 1;` under `port < 0` shows `#ret == 0
&& port == -1`.
- **Never array values.** Only Z3 can read them. `TranslatorToZ3` now
skips array-sorted model values, as it already skipped uninterpreted
sorts. Their ghosts (`length(a)`) remain.

**Order**, most relevant first:

1. Terms of Expected that Found says nothing about.
2. The other terms of Expected.
3. The linked terms, in the order the variables were introduced (the
binder order of the VC chain before simplification).
4. Generated `#fresh` names last.

**Display.** `VariableFormatter.format` formats ghost application
arguments (`size(#s_3)` becomes `size(s³)`). It uses a scanner that only
splits top-level commas, so `f(g(#a_1, #b_2), #c_3)` becomes `f(g(a¹,
b²), c³)`. The CLI uses this, and so does the VS Code server's
`CounterexampleDTO`. The fresh-name prefix now lives in
`Formats.FRESH_PREFIX`, shared with `VCBinderSimplification`.

### Behaviour changes in existing outputs

Sweep of main against this PR over 149 `Error*` testSuite entries, 25
`ErrorCounterexample*` fixtures and 97 study exercises (257 entries,
main at `19991d36`): **70 outputs change**.

- **21 change order only.** The same values come back, with Expected's
values (often `#ret`) now first and `#fresh` last:
- fixtures: `ErrorAfterIf`, `ErrorAssignmentBeforeReturn`,
`ErrorBitwiseUnknownOperand`, `ErrorBoolean`,
`ErrorCharLiteralComparisons`, `ErrorDeferredCallbackState`,
`ErrorDependentUpperBound`, `ErrorEmptyLoopBody`,
`ErrorFieldOfOtherObject`, `ErrorIdentity`, `ErrorIntegerDivision`,
`ErrorOperatorAssignments`, `ErrorRecursion`, `ErrorRecursiveDecrement`,
`ErrorRecursiveSiblingParameter`, `ErrorUnknownMethodInOperation`
  - exercises: `E_A2_03`, `E_A2_07`, `E_A2_08`, `E_A2_10`, `E_OSS_A2_05`
- For example, `x == 1 && #ret² == 0` becomes `#ret² == 0 && x == 1`.
The 7 affected `TestCounterexamples` assertions are updated.
- Of these, **five fixtures reorder because `#fresh` now goes last**:
`ErrorBitwiseUnknownOperand`, `ErrorFieldOfOtherObject`,
`ErrorNullLiterals`, `ErrorUnknownMethodInOperation` and
`ErrorCounterexampleCallArgument`. The first version of this PR body did
not say so.
- **49 change content.** These are the new fixtures, plus:
- values Expected needs that were missing:
`ErrorUnconstrainedRefinement`, `ErrorUnknownArgument`,
`ErrorUnresolvedOperationValue`, `ErrorEnumConstantInCondition`,
`E_OSS_A1_05`, `E_OSS_A2_04`
- unlinked path values dropped: `ErrorLoopCondition`, `ErrorInstanceof`,
`ErrorUnknownMethodInComparison`, `E_A2_02`, `E_OSS_A2_01`, plus
counterexamples made only of an opaque `#fresh` value that Expected does
not depend on: `ErrorNullLiterals` (two of its errors; the others only
reorder), `ErrorUnresolvedBinaryOperator`,
`ErrorUnresolvedFieldDeclaringType`, `ErrorUnresolvedUnaryOperator`
- known enum values no longer repeated: `ErrorEnumFunctionRefinement`,
`ErrorEnumNegation`, `ErrorLocalShadowsConstant`, and the first error of
`ErrorEnumConstantInCondition`
- array values replaced by `length(…)`, or dropped when the length is
known: `ErrorSearchIntArray`, `ErrorImplementationSearchValueIntArray`,
`ErrorSearchValueIntArray`, `ErrorStringArrayLength`,
`ErrorLenZeroIntArray`
  - `ErrorEnumNull`, which is a known limitation (see below)

### Relation to #299 and #459

- **#299** substitutes the filtered counterexample into the final
Expected. With this change it has the value it needs: the reproducer
would show `With witness: -1 >= 0 ✗` (checked earlier with a trial
merge). It conflicts textually with this PR:
- In `RefinementError`, both add imports, and #299 inserts
`substituteWitness` right above the comment this PR rewrites. Keep both
sides.
- In `TestCounterexamples`, #299 extends `dependentUpperBound…`, which
this PR renames and reorders. Keep #299's extra assertions on the
renamed test.
- **#459** merges cleanly in `VariableFormatter`,
`VariableFormatterTest` and `VCBinderSimplification`. The application
formatting is one early branch plus private methods at the end of the
class, with no new imports. Its `TestFoundBinders` has 3 assertions that
pin the old order (`a == 0 && this.amount == 0`, `count == 0 &&
Basket.served == -1`, `y == 0 && x == -1`). Whichever PR lands second
flips those three to Expected-first; nothing else changes (checked with
a trial merge).

## Tests

**25 testSuite fixtures** (`ErrorCounterexample*.java`, each with `//
Expect: Refinement Error`) plus matching `TestCounterexamples` cases
that assert the exact assignments:

| Fixture | main | this PR |
|---|---|---|
| `UnconstrainedArgument` (issue reproducer) | `port == 0` | `timeout ==
-1` |
| `CombinedGuard` (`if (port<0 \|\| … \|\| window<1 \|\| timeout>60000)
return;`) | `port == 0 && retries == 0 && backoff == 0 && window == 1` |
`timeout == -1` |
| `MixedGuard` (`port<0 \|\| (retries>3 && backoff>10) \|\|
timeout>60000`) | `port == 0 && retries == 0` | `timeout == -1` |
| `GuardRelatesArguments` (`retries > timeout + 5`) | `port == 0 &&
retries == 0` | `timeout == -1 && retries == 0` |
| `NothingKnown` (Found is `true`) | *(none)* | `millis == -1` |
| `GuardedArgument` | `port == 0` | `timeout == -1` |
| `AliasedArgument` | `configured, port, timeout¹¹` | `timeout¹¹ == -1
&& configured == -1` |
| `FieldArgument` | `this#…timeout, port, timeout⁶` | `timeout⁶ == -1 &&
this#…timeout == -1` |
| `CallArgument` (`connect(read(key) - 1)`) | `#fresh⁶, port, timeout⁷`
| `timeout⁷ == -1 && #fresh⁶ == 0` |
| `BranchArgument` (nested if/else) | `secure == false && #fresh⁰ ==
false && port == 1025` | `timeout == -1` |
| `SeveralArguments` | `port == 0 && lo == 1` | `hi == 0 && lo == 1` |
| `KnownArgument` | `port == 0` | `capacity == 0` |
| `LinkedPathCondition` (`connect(port - 1)`) | `port, retries,
timeout¹⁰` | `timeout¹⁰ == -1 && port == 0` |
| `ReturnPath` | `configured, port, #ret⁵` | `#ret⁵ == -1 && configured
== -1` |
| `ReturnConstant` (`return 0` under `port < 0`) | `port == -1` |
*(none)*: Found fixes `#ret == 0` |
| `ReturnFromPath` (`return port + 1` under `port < 0`) | `port == -1 &&
#ret² == 0` | `#ret² == 0 && port == -1` |
| `KnownGuardedArgument` (`int value = 0; if (port > 0) take(value);`) |
`port == 1` | *(none)* |
| `KnownTwiceGuardedArgument` (same, under two guards) | `port == 1 &&
retries == 0` | *(none)* |
| `KnownAliasedArgument` (`int base = 0; int value = base;`) | `port ==
1` | *(none)* |
| `RefinementAlias` | `port == 0` | `timeout == -1` |
| `GhostArgument` | `port == 0` | `size(bag) == 0` |
| `KnownGhost` (Found states `size(s⁹) == 1`) | `port == 0` | *(none)* |
| `KnownEnum` (`format == Format.JPG`) | *(none)* | *(none)*; `format ==
JPG` stays hidden |
| `ArrayArgument` (`get(a, 3)`) | `port == 0` | `length(a) == 0` |
| `ArrayIndex` (`int[] a = new int[4]; get(a, k)`) | `port == 0 && a⁵ ==
((as const (Array Int Int)) 4)` | `k == -1` |

**15 unit tests** in `RefinementErrorCounterexampleTest`. Each builds a
`RefinementError` from a VC chain and a hand-written model. They cover:

- an Expected variable that simplification dropped
- unlinked facts
- equality chains
- unmentioned path binders
- generated names ordered last
- known values, known enum values, and known ghosts with several
arguments (and the unknown case)
- splitting negated disjunctions, nested conjunctions and double
negations
- a guard that relates Expected to another variable
- no counterexample when Found fixes every linked value, even with a
path condition, and a path condition Expected's value is computed from

`VariableFormatterTest` also covers nested applications.

The review fixtures fail on the commit before them: `CombinedGuard`,
`MixedGuard`, `GuardRelatesArguments`, `KnownEnum`, `ArrayArgument` and
`ArrayIndex` on `491d297e`; `KnownGuardedArgument`,
`KnownTwiceGuardedArgument` and `KnownAliasedArgument` on `9e037b6b`,
which showed `port == 1`. So do their unit tests. Four tests guard
behaviour that should not change and pass on both: `ReturnFromPath`,
`keepsAPathConditionTheExpectedValueIsComputedFrom`,
`hasNoCounterexampleWhenFoundStatesEveryValue` and
`keepsGhostValuesWithSeveralArgumentsFoundSaysNothingAbout`.

`mvn test` (verifier): **599 tests, 0 failures, 0 errors** (534 on
main).

### CLI before / after

Issue reproducer:

```
Refinement Error: !(port < 0 || port > 65535) is not a subtype of timeout >= 0
- --> Counterexample: port == 0
+ --> Counterexample: timeout == -1
```

OpenNMS study exercise (`E_OSS_A2_04_VmwareCimProbe`):

```
- --> Counterexample: #fresh³¹⁶ == false && port³¹³ == 0
+ --> Counterexample: timeout == -1
```

Combined guard:

```
Refinement Error: !(port < 0 || port > 65535 || retries < 0 || backoff < 0 || window < 1 || timeout > 60000) is not a subtype of timeout >= 0
- --> Counterexample: port == 0 && retries == 0 && backoff == 0 && window == 1
+ --> Counterexample: timeout == -1
```

Array index:

```
Refinement Error: !(port < 0) && length(a⁵) == 4 is not a subtype of k >= 0 && k < length(a⁵)
- --> Counterexample: port == 0 && a⁵ == ((as const (Array Int Int)) 4)
+ --> Counterexample: k == -1
```

Ghost state:

```
Refinement Error: !(port < 0) is not a subtype of size(bag) > 0
- --> Counterexample: port == 0
+ --> Counterexample: size(bag) == 0
```

Known enum value (`ErrorEnumFunctionRefinement`):

```
Refinement Error: newColor¹¹ == Blue is not a subtype of newColor¹¹ == Color.Red || newColor¹¹ == Color.Green
- --> Counterexample: newColor¹¹ == Blue
+ (no counterexample: Found already states it)
```

### Left out, and why

- **`ErrorEnumNull`** (`Color c = null`) now shows `c³ == Blue`. Found
is `true` because the verifier does not model `null` for enums; the
assignment is lost before the error is built. `Blue` is a real
counterexample to what Found states, but not the value the program has.
Hiding values whenever Found is `true` would also hide `millis == -1` in
the issue's own case. The fix belongs in how `null` enum assignments are
translated, which is a separate issue.
- **Typestate parameters** (`@Refinement("open(f)")`): `RefinementError`
receives Expected before states are expanded, while the model names the
state ghost `state1(#f_6)`. Here Found already states that ghost
(`closed(f⁶)` is `state1 == 0`), so nothing new would be shown even
after expansion, and `state1(f⁶) == 0` would be harder to read than the
state name. With nothing new to show, there is no counterexample (main
showed the unrelated `port == 0`). Showing values in state names needs
the state mapping in the error, which this PR does not add.
- **No counterexample, rather than the known value, when Found fixes
Expected.** Repeating `value == 0` would only restate Found, and it is
the rule `ErrorLiteralZero` and `ErrorStaticFinalConstant` already pin.
The cost is `ten(port)` with `return 0;` under `port < 0`
(`ReturnConstant`): main showed `port == -1`, which says which return
failed. The VC cannot tell that case apart from `take(value)` under
`port > 0`, where `port == 1` misleads. In both, a guard is unlinked to
an Expected term that Found fixes. When the return value is computed
from the path (`return port + 1;`), the path value is linked and shown.
- **Ghost applications whose arguments are not plain variables**
(`size(old(this))`) are not matched. The model names them by Z3's
rendering of the argument.
- **`!(x != v)` is not rewritten to `x == v`.** Hiding that value would
hide the breaking value itself (`t == -3` against `t >= 0`).
- Declaring a ghost class as a nested `static class` makes Z3 fail with
`Sort mismatch … supplied sort is …$Bag`. This is an unrelated, existing
bug, so the ghost fixtures use top-level classes.

Fixes #453

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>

…472)

## Problem

After #459, Found still shows `true` rows for variables that another row
already shows (#375):

- **A1_56** (JabRef `EditAction`, state error): `∀getUndoManager true`.
- **A1_09** (`PlayfieldWindow`, state error): `∀previousMode true`,
`∀DisplayMode.BORDERLESS true` and `∀newMode true`, above the ternary
that uses them.

#459 kept a `true` binder when a fact linked to Expected constrains its
value. That fact is always a row the user already sees, and it already
names the variable. So the extra `true` row adds no fact. It also reads
as if the variable's value were `true`, which is what #375 is about. The
A1_09 rows are not needed: the ternary row shows `previousMode`,
`newMode` and `BORDERLESS`, and that row explains why `host` may still
be displayable. `DisplayMode.BORDERLESS` is an enum constant, so a
binder row for it says nothing.

## Rule

A binder refined only by `true` is shown only when **all** of these
hold:

1. the error is a refinement error, so it has a counterexample;
2. Expected constrains the variable's value;
3. **no other row of Found mentions the variable.**

When all three hold, the row is the only place the variable appears in
Found. It tells the user that nothing is known about a value the error
depends on (`∀t true`, counterexample `t == 0`). In every other case the
row goes, because the variable is either shown in the rows that use it
or not needed.

No variable disappears from what the user sees:
- A dropped binder's variable still appears in the rows that mention it.
- The counterexample is unchanged.
`RefinementError.filterCounterexample` takes its terms from Expected and
from Found's facts, not from the binders, so for example `Basket.served
== -1` still shows after its row goes.

`NeededVariables` no longer links facts to Expected. Two pieces of code
had no other use, so this PR removes them:
- `splitConjuncts` and `linkedConjuncts` in `VCSimplificationUtils`;
- the `VCBinderOrdering` pass and its test. That pass only moved kept
`true` binders before their first use. A kept binder now has no other
use, so the pass could never fire.

## Before / after

**A1_56** (`undoManager.redo()` on a manager from a getter)
```
before: ∀getUndoManager¹²⁹   true
        ∀#fresh¹¹²           !#fresh¹¹¹
        ∀#fresh¹²⁶           !(#fresh¹²⁴ || #fresh¹²⁵)
        ∀undoManager¹³¹      undoManager¹³¹ == getUndoManager¹²⁹
after:  ∀#fresh¹¹²           !#fresh¹¹¹
        ∀#fresh¹²⁶           !(#fresh¹²⁴ || #fresh¹²⁵)
        ∀undoManager¹³¹      undoManager¹³¹ == getUndoManager¹²⁹
```

**A1_09** (`host.setUndecorated(true)` after a conditional `dispose()`)
```
before: ∀previousMode            true
        ∀DisplayMode.BORDERLESS  true
        ∀newMode                 true
        ∀host¹²¹   previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host¹²¹) : (previousMode != BORDERLESS && newMode == BORDERLESS ? notDisplayable(host¹²¹) : displayable(host¹²¹))
after:  ∀host¹²¹   previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host¹²¹) : (previousMode != BORDERLESS && newMode == BORDERLESS ? notDisplayable(host¹²¹) : displayable(host¹²¹))
```

**Test suite fixture** (`classes/found_binders_error`)

| Case | before | after |
|---|---|---|
| `int sum = first + second` refined `_ > 0` (new) | `∀first true`,
`∀second true`, `∀sum sum == first + second` | `∀sum sum == first +
second`, counterexample `sum == 0 && first == 0 && second == 0`
(unchanged) |
| `int count = served + 1` (static field) | `∀Basket.served true`,
`∀count count == Basket.served + 1` | `∀count count == Basket.served +
1`, counterexample `count == 0 && Basket.served == -1` (unchanged) |
| `positive(t)` with `t` unconstrained (new, kept) | `∀t true`,
counterexample `t == 0` | same |

In the same way, `ErrorStateHintPathDependent` now shows only `ready ?
open(f) : created(f)`, without `∀ready true`.

What the fixed `#fresh` path rows still show (`∀#fresh¹¹² !#fresh¹¹¹`)
is the separate part of #375 that ties in with #373. They are not `true`
rows, and this PR leaves them alone.

## Tests

- `TestFoundBinders`:
- `variablesAnotherRowShowsGetNoTrueRow` (positive): new `addUp`
fixture, the A1_09 pattern as a refinement error.
- `variableOnlyExpectedNamesKeepsItsTrueRow` (negative): new `forward`
fixture. The informative `∀t true` row and its counterexample stay.
- `staticFieldIsWrittenWithItsClass` updated: the `Basket.served` row
goes, and its counterexample value stays.
- `VCBinderSimplificationTest`:
- Tests that encoded the old linking rule now expect the row to go:
`removesTrueBinderThatALaterRowShows`,
`removesTrueBinderThatIsTheArgumentOfAGhost`, and
`removesTrueBindersThatAConditionalStateShows` (the A1_09 shape).
  - New `removesTrueBinderOfExpectedVariableThatAnotherRowShows`.
- `keepsTrueBinderOfExpectedVariableNoOtherRowMentions` (renamed) still
keeps the row.
- `skipsInapplicableTrueBinderAndSimplifiesLaterBinder` now uses a row
that does not mention `x`, so `x` is still the inapplicable binder.
- Without the fix (`main` sources, new tests kept), 6 of the 22 tests in
these two classes fail, including both positive tests. The negative test
passes on both, as it should.
- `mvn test`: **667 tests, 0 failures.**

Part of #375. The `#fresh` path rows are left for #373.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>

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](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>

## Problem

When a call argument is itself a call, the refinement error named its
value after the callee's parameter (`bound`), which is not in the
caller's code.

## Before / after

Issue reproducer (`return nextInt(size());`):

```
before: bound³ >= 0 is not a subtype of bound³ > 0
        Counterexample: bound³ == 0
after:  size()³ >= 0 is not a subtype of size()³ > 0
        Counterexample: size()³ == 0
```

Real case, fixture `classes/found_binders_error`
(`random.nextInt(items.size())`, as in chaos-http-proxy's
`failures.size()`):

```
before: bound⁶ == size(this.items) && bound⁶ >= 0 is not a subtype of bound⁶ > 0
        ∀bound⁶   bound⁶ == size(this.items) && bound⁶ >= 0
        Counterexample: bound⁶ == 0
after:  items.size()⁶ == size(this.items) && items.size()⁶ >= 0 is not a subtype of items.size()⁶ > 0
        ∀items.size()⁶   items.size()⁶ == size(this.items) && items.size()⁶ >= 0
        Counterexample: items.size()⁶ == 0
```

Nested calls: `nextInt(dec(size()))` gives `size()¹⁹ >= 0 &&
dec(size())²¹ == size()¹⁹ - 1 is not a subtype of dec(size())²¹ > 0`. An
unrefined call reads `plain()⁸ == #plain_result⁷` (result name from
#483).

The argument keeps its instance counter, like every other instance, so
two calls written alike (`between(next(), next())`) stay apart.

## Unchanged

Plain variables (`positive(t)`), field reads (`bound == this.f`), other
expressions (`bound == this.f - 1`) and literals keep the parameter
name: their refinement is `bound == <their code>`, so writing them as
code would read as a tautology (`0 == 0`, which `TestGeneratedNames`
would catch).

## How

Same approach as `FieldDisplayNames` (#459): `MethodsFunctionsChecker`
records the call's source text as written (Spoon's original source
fragment, so `count()` is not printed as `Basket.count()`) for the
argument instance in the new `ArgumentDisplayNames`.
`VariableFormatter.format` writes it with the counter, and
`ExpressionNameResolver` keeps it whole, as it does for fields
(`items.size()` is not cut to `size()`). A call with no source position
(built by Spoon, not read from a file) keeps the parameter name.
`CommandLineLauncher` clears the record at the start of each run. The
internal name and the SMT query are unchanged.

## Size

+68 / −7 over 7 files (main code +48 / −2; the new
`ArgumentDisplayNames` is 35 of those lines, most of them Javadoc).

## Tests

- `TestFoundBinders`: the reproducer's rows (also in the original step
of the history) now use `items.size()`; new
`callArgumentIsWrittenAsTheCallerWroteIt` on a new fixture line
`random.nextInt(count())`, checking the message and counterexample read
`count()`, not `bound` or `Basket.count()`.
- All of them fail on `main`, and the rows fail without the
`ExpressionNameResolver` change.
- `mvn test`: 693 tests, 0 failures.

Closes #481

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>