Impact: Found lists facts about variables that the expected refinement does not mention, and nothing about the one it does. It is the first thing a reader reads, and it points them away from the problem. The counterexample (since #453) and the hints are right; Found is what misleads.

Minimal reproducer 1 (refinement)

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);
    }
}

Actual (main @ cd49fea):

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

Minimal reproducer 2 (state)

import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"empty", "full"})
class Box {
    @StateRefinement(to = "empty(this)")
    Box() {}

    @StateRefinement(to = "full(this)")
    void put() {}

    @StateRefinement(from = "full(this)", to = "empty(this)")
    void take() {}
}

public class Probe {
    Box box = new Box();

    Box getBox() { return box; }

    void run(String a, String b) {
        Box box = getBox();
        if (a.isEmpty() || b.isEmpty()) return;
        box.take();
    }
}

Actual (main @ cd49fea):

State Refinement Error: found !(#isEmpty_result¹⁶ || #isEmpty_result¹⁷) && box¹⁵ == getBox¹³ but expected full(box¹⁵)
Hints:
  - The state of box is unknown here, and this call needs it to be full
  - Call box.put() before this call to move box from any state to full

Expected: Found keeps the facts about the variables of the expected refinement (timeout; the state of box) and drops the rest, or says that nothing is known about them, e.g. found timeout (no constraint) but expected timeout >= 0 and found box in an unknown state but expected full(box). Path conditions about other variables can stay in the derivation or the IDE's detail view.

Related: #374 (keep the target variable in Found).

Real-world scenario. Two of the six exercises for the error-message study:

• OpenNMS VmwareCimProbe: socket.connect(new InetSocketAddress(host, port), timeout) with a configured timeout of -1, which throws IllegalArgumentException: connect: timeout can't be negative. Found is all about the port: !(#operation_result⁷¹ || port⁶⁵ < 0 || port⁶⁵ > 65535) is not a subtype of timeout >= 0, so the reader starts checking the port guard.
• JabRef EditCommand: undoManager.redo() with nothing to redo (fix: guard with canRedo()). Found is !#operation_result¹³³ && !(#operation_result¹⁴⁶ || #operation_result¹⁴⁷) && undoManager¹⁵³ == getUndoManager¹⁵¹ but expected redoable(undoManager¹⁵³): the results of three unrelated calls in the same method, none of which says anything about the manager's state.