GeezerVison

## 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]>