Internal error "Expr cannot be cast to BoolExpr" on a local assigned from an array element (Res r = rs[0]) #437

Impact: internal error on any check that involves a local holding an array element. A check that should pass fails (false error), and a real violation there is shown as an internal error instead of a refinement or state error.

Description

RefinementTypeChecker.visitCtArrayRead (RefinementTypeChecker.java:273) sets the element's refinement to the bare variable arrayAccess_N instead of _ == arrayAccess_N. Passing xs[0] directly to a call works, but after int c = xs[0] (or Res r = rs[0], var c = objs[0]), c's refinement is that non-boolean term, and the first SMT check that includes it fails with a Z3 ClassCastException: IntExpr for an int[], Expr for an object array. Setting the metadata to _ == arrayAccess_N would probably fix it.

Minimal reproducer (typestate)

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

@StateSet({"open", "closed"})
class Res {
    @StateRefinement(to = "open(this)")
    public Res() {}

    @StateRefinement(from = "open(this)")
    public void read() {}

    @StateRefinement(from = "open(this)", to = "closed(this)")
    public void close() {}
}

public class Repro {
    void f(Res[] rs) {
        Res r = rs[0];
        r.close();
        r.read();
    }
}

Expected

A State Refinement Error at r.close(), as when r is a parameter (control below).

Actual

Error: class com.microsoft.z3.Expr cannot be cast to class com.microsoft.z3.BoolExpr (com.microsoft.z3.Expr and com.microsoft.z3.BoolExpr are in unnamed module of loader 'app')
17 |     void f(Res[] rs) {
18 |         Res r = rs[0];
19 |         r.close();
   |         ^^^^^^^^^^
20 |         r.read();
21 |     }

Control: the same calls on a parameter Res r

State Refinement Error: found true but expected open(r⁹)

Smaller form, without typestate

import liquidjava.specification.Refinement;

public class Repro {
    static void positive(@Refinement("_ > 0") int x) {}

    void f(int[] xs) {
        int c = xs[0];
        positive(c);
    }
}

Error: class com.microsoft.z3.IntExpr cannot be cast to class com.microsoft.z3.BoolExpr (com.microsoft.z3.IntExpr and com.microsoft.z3.BoolExpr are in unnamed module of loader 'app')
 6 |     void f(int[] xs) {
 7 |         int c = xs[0];
 8 |         positive(c);
   |         ^^^^^^^^^^^^

The reviewers' forms Res r = s.get()[0] (Supplier<Res[]>), Res r = rs[s.getAsInt()], and var c = objs[0]; any(c) (Object[]) give the same error.

Reproduced on main at 1a506fe (liquidjava-verifier 0.0.36).

Context

Found while reviewing #432. Related: #425 (crash on an array read whose element type cannot be resolved).

🤖 Generated with Claude Code