Two problems with what an UNKNOWN refinement error shows.

1. The general hint. A2_04 (Socket.connect(..., @Refinement("_ >= 0") int timeout), where timeout is an unrefined parameter) prints:

Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.

Both routes it suggests are graded wrong in the study:

• a refinement on the method's parameter moves the error to the callers and goes against the Javadoc;
• a condition such as an early return skips the probe.

The hint is not specific to the task, and it pulls participants away from the fix.

2. Declared-here shows only one from. When Expected is the disjunction of several @StateRefinement froms (A1_01: lines 110–111, compressionExplicit || compressionTypeSet), the declared-here excerpt and the where … means … gloss show only the first. They come from a findFirst() in AuxStateHandler.

Proposal

• Drop that general hint.
• Show every from that makes up Expected in declared-here, each with its gloss.