Counterexample leaves out the variable the expected refinement constrains, when Found knows nothing about it #453

Impact: when nothing is known about the variable a refinement constrains, the counterexample leaves that variable out and shows values for unrelated path conditions instead. The reader is pointed away from the value that breaks the call.

Minimal reproducer

import liquidjava.specification.Refinement;

public class Probe {
    static void connect(@Refinement("_ >= 0") int timeout) {}

    static void probe(int port, int timeout) {
        if (port < 0 || port > 65535) return;
        connect(timeout);
    }
}

Expected: the counterexample names timeout, e.g. Counterexample: timeout == -1 (with or without port).

Actual (main @ 19991d3):

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

Cause. RefinementError.filterCounterexample keeps only assignments to the binders of the simplified Found. timeout is known only as true, so simplification drops its binder, and its assignment is filtered out with it. Keeping assignments to the variables of the expected refinement (even when Found no longer binds them) would fix it. Related: #296 / #299 (substituting the counterexample into the expected refinement), which needs timeout in the counterexample to show -1 >= 0.

Real-world scenario. One of the exercises for the error-message study is OpenNMS's VMware probe: socket.connect(addr, timeout) with a configured timeout of -1, which throws IllegalArgumentException: connect: timeout can't be negative. The IDE panel shows Counterexample: #fresh == false, port == 0, which sends the reader to the port guard. The only variable that matters, timeout, isn't there.

In VS Code (OpenNMS study exercise, verifier main @ 19991d3, extension main @ 80bed18). The counterexample shows #fresh¹²⁵⁶ == false and port¹²⁵⁰ == 0 for timeout >= 0: