Impact: when the argument of a call is itself a call or an expression, the message is written entirely in terms of the callee's parameter name (bound), which does not appear anywhere in the caller's code. The reader has to work out that bound is the parameter of nextInt and that it stands for size() here, before they can read the error.

Minimal reproducer

import liquidjava.specification.Refinement;

public class Probe {
    @Refinement("_ >= 0 && _ < bound")
    static int nextInt(@Refinement("_ > 0") int bound) { return 0; }

    @Refinement("_ >= 0")
    static int size() { return 0; }

    static int pick() {
        return nextInt(size());
    }
}

Actual (main @ cd49fea):

Refinement Error: bound³ >= 0 is not a subtype of bound³ > 0
11 |         return nextInt(size());
   |                ^^^^^^^^^^^^^^^
 --> Counterexample: bound³ == 0

Expected: the message names the argument as written at the call site, e.g. size() >= 0 is not a subtype of size() > 0 with Counterexample: size() == 0, or keeps the parameter but says what it is: bound (the argument size() of nextInt) >= 0 is not a subtype of bound > 0. The underline could also cover just the argument (size()) rather than the whole call.

Real-world scenario. chaos-http-proxy's RandomFailureSupplier, an exercise for the error-message study: failures.get(random.nextInt(failures.size())) throws IllegalArgumentException: bound must be positive when every failure is configured off and the list is empty (fix: if (failures.isEmpty()) return Failure.SUCCESS;). The message is

Refinement Error: bound⁸³ == size(this.failures) && bound⁸³ >= 0 is not a subtype of bound⁸³ > 0
 --> Counterexample: bound⁸³ == 0

bound is the parameter name in the java.util.Random spec; the participant's code only has failures.size(). failures.size() == 0 would point straight at the bug.