False error: comparing with a char literal other than a lowercase letter, digit or _ ('[', 'Z', ' ') is rejected as an invalid refinement expression #444

Impact: correct client code is rejected with a syntax error whenever it compares a char with a literal like '[', '{', ',', ' ' or 'Z', which is the everyday code of parsers and tokenizers. No annotations are involved. This is related to #398 (escaped literals such as '\r'), but it is broader: plain punctuation, the space and uppercase letters fail too.

Minimal reproducer

public class Repro {
    static int skipTo(String s) {
        int i = 0;
        while (s.charAt(i) != '[')
            i++;
        return i;
    }
}

Expected: Correct! Passed Verification.

Actual (main @ f7f366c, and 1a506fe):

Syntax Error: Invalid refinement expression, expected a logical predicate

Which literals fail. return s.charAt(i) == C; was tried for each literal C:

The ones that pass are exactly the characters that can start an ID or an INT in RJ.g4, which has no char-literal token. That suggests the literal reaches the refinement parser as text. If so, '0' "passing" may also give it the value 0 rather than 48. I haven't checked that.

Real-world scenario. I found this while checking real client code against a java.io.BufferedReader spec. Two methods from FrancescoBorzi/Esercizi-Tecniche-di-Programmazione-Concorrente-e-Distribuita (es05.java, es11.java) read an HTTP response with readLine() and then scan it for a bracket:

BufferedReader in = new BufferedReader(new InputStreamReader(client.getInputStream()));
...
msg = "";
while ((tmp = in.readLine()) != null)
    msg += tmp;

i = 0;
while (msg.charAt(i) != '[')     // Syntax Error here
    i++;

The reader is used correctly, but the method can't be verified at all, so the typestate check of in never happens. JSON and CSV tokenizers (c == '{', c == ',', c == ' ') hit the same error.