Impact: correct code is rejected (false error).

Description

length(x) is not known to be non-negative, so the solver picks a negative length. Any refinement that needs length(a) >= 0 must be written out by hand.

Minimal reproducer

import liquidjava.specification.Refinement;

class Len {
    @Refinement("_ >= 0")
    static int size(int[] names) {
        return names.length;
    }
}

Expected

Correct! Passed Verification.

Actual (main ad055b4)

Refinement Error: #ret⁰ == length(names) is not a subtype of #ret⁰ >= 0
 --> Counterexample: names == ((as const (Array Int Int)) (- 1)) && #ret⁰ == -1

Possible fix

Assume length(x) >= 0 for every array variable when it enters the context, or add the axiom in the SMT translation of length.