Verifier crashes with a sort mismatch on .length of a non-int array #355

length is declared for int arrays only ((declare-fun length ((Array Int Int)) Int)). When an array of any other element type has its .length in the context (e.g. in a loop condition) and the verifier then sends a query to Z3, it crashes with a sort mismatch.

Example

With the Throwable spec (initCause from noThrowable to withThrowable):

public class Repro {
    static void chain(String[] names) {
        for (int i = 0; i < names.length; i++) {
            Exception e = new Exception(names[i]);
            e.initCause(null);
        }
    }
}

On main (be47cb6):

Error: Sort mismatch at argument #1 for function (declare-fun length ((Array Int Int)) Int) supplied sort is |java.lang.String[]|

The same method with int[] names passes. Real code loops over object arrays all the time (for (int i = 0; i < arr.length; i++) over File[], String[], …); this blocked an exercise built from a NetBeans bug that loops over an InstanceCookie[]. Earlier we saw the same crash with byte[].length passed to a refined parameter.

Expected

Declare length per array sort (or use one polymorphic declaration), so .length works for any element type.