Crash: an array initializer (new T[] {...}) passed to a parameter refined with length() gives "Sorts ... and Bool are incompatible" #448

Impact: a correct call is rejected with an internal Z3 error whenever an array initializer is passed to a parameter whose refinement mentions length() of that array. This hits every array type, including int[]. new byte[2] and a variable both work. This is not #355, which was about .length of non-int arrays and is closed.

Minimal reproducer

import liquidjava.specification.Refinement;

public class Repro {
    static void put(byte[] b, @Refinement("_ >= 0 && _ <= length(b)") int n) { }

    public static void main(String[] args) {
        put(new byte[] {1, 2}, 2);
    }
}

Expected: Correct! Passed Verification.

Actual (main @ f7f366c, and 1a506fe):

Error: Sorts |byte[]| and Bool are incompatible

Real-world scenario. I found this while checking a spec of java.io.PipedOutputStream. Its write(byte[] b, int off, int len) throws IndexOutOfBoundsException unless the range is inside the array, so the spec refines off and len:

void write(byte[] b, @Refinement("_ >= 0") int off, @Refinement("_ >= 0 && off + _ <= length(b)") int len);

Writing a small literal message, a common way to send a header or a test payload, then fails with the error above:

PipedOutputStream o = new PipedOutputStream(new PipedInputStream());
o.write(new byte[] {1, 2}, 0, 2);           // runs fine; LiquidJava: Sorts |byte[]| and Bool are incompatible

The same refinement works when the array is created with a size (new byte[4]) or held in a variable. So the out-of-range check is useful, but it breaks on literal arrays.