Error messages show a named constant as its value (mode == 2 instead of mode == ImageWriteParam.MODE_EXPLICIT) #488

Impact: a named constant that the client code passes is shown as its value. The reader sees mode == 2, but their code says ImageWriteParam.MODE_EXPLICIT and they have no reason to know that it is 2. The value is also implementation-dependent. The spec side keeps the name, because it is printed from the spec text, so the two sides of one message don't even match.

Minimal reproducer

import javax.imageio.ImageWriteParam;

import liquidjava.specification.Refinement;

public class Probe {
    static void setProgressiveMode(@Refinement("_ != ImageWriteParam.MODE_EXPLICIT") int mode) {}

    static void direct() {
        setProgressiveMode(ImageWriteParam.MODE_EXPLICIT);
    }

    static void throughLocal() {
        int mode = ImageWriteParam.MODE_EXPLICIT;
        setProgressiveMode(mode);
    }
}

Actual (main @ cd49fea), for both methods:

Refinement Error: mode == 2 is not a subtype of mode != ImageWriteParam.MODE_EXPLICIT

Expected:

Refinement Error: mode == ImageWriteParam.MODE_EXPLICIT is not a subtype of mode != ImageWriteParam.MODE_EXPLICIT

Rule. Keep a constant's name in Found, Expected, the derivation steps and the counterexample wherever the code or the spec wrote it, whatever the operator. The SMT encoding still uses the value. Names come only from where the source wrote them, never from matching a value: several constants can share the value 2. Numbers stay numbers when they really are numbers: computed values (MODE_EXPLICIT + 1), literals the code wrote, and values the solver makes up in a counterexample. The displayed formula must stay a valid refinement expression, so the simplification steps can keep working on it. No (2) annotations.

Where the name is lost. Predicate resolves static final constants to literals when it reads them (StaticConstants.resolve / asLiteralPredicate), so the name is gone before the VC is built and simplified.

Real-world scenario. In the error-message study, the dcm4che task (javax.imageio.ImageWriteParam) is fixed with setCompressionMode(ImageWriteParam.MODE_EXPLICIT), and the spec's mode refinements are written with the MODE_* constants (liquid-java/co-specification#94, #96). A participant who passes the wrong mode should see the constant they wrote.