Support length on arrays of any element type

liquidjava-example/src/main/java/testSuite/CorrectStringArrayLength.java

@@ -0,0 +1,20 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectStringArrayLength {
+
+    static int nonNegative(@Refinement("_ >= 0") int x) {
+        return x;
+    }
+
+    public static int count(@Refinement("length(names) > 0") String[] names) {
+        int n = 0;
+        for (int i = 0; i < names.length; i++) {
+            n = nonNegative(i - i);
+        }
+        @Refinement("_ > 0")
+        int size = names.length;
+        return n + size;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorStringArrayLength.java

@@ -0,0 +1,11 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorStringArrayLength {
+
+    public static void first(@Refinement("length(names) >= 0") String[] names) {
+        @Refinement("_ > 0")
+        int size = names.length; // Expect: Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -39,6 +39,7 @@ public class TranslatorToZ3 implements AutoCloseable {
     private final Map<String, List<Expr<?>>> varSuperTypes = new HashMap<>();
     private final Map<String, AliasWrapper> aliasTranslation = new HashMap<>(); // this is not being used
     private final Map<String, FuncDecl<?>> funcTranslation = new HashMap<>();
+    private final Map<Sort, FuncDecl<?>> lengthBySort = new HashMap<>();
     private final Map<String, Expr<?>> funcAppTranslation = new HashMap<>();
     private final Map<Expr<?>, String> exprToNameTranslation = new HashMap<>();
     /**
@@ -163,6 +164,8 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws LJEr
             return makeStore(params);
         if (name.equals("getFromIndex"))
             return makeSelect(params);
+        if (name.equals("length") && params.length == 1)
+            return makeLength(params[0]);
         FuncDecl<?> fd = funcTranslation.get(name);
         if (fd == null)
             fd = resolveFunctionDecl(name, params);
@@ -185,6 +188,20 @@ public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws LJEr
         return app;
     }
 
+    /**
+     * Applies {@code length} to an array of any element type: the builtin declaration covers {@code int[]} only, so
+     * other array sorts get their own overload, declared on first use.
+     */
+    private Expr<?> makeLength(Expr<?> array) {
+        Sort sort = array.getSort();
+        FuncDecl<?> fd = funcTranslation.get("length");
+        if (!fd.getDomain()[0].equals(sort))
+            fd = lengthBySort.computeIfAbsent(sort, s -> z3.mkFuncDecl("length", s, z3.getIntSort()));
+        Expr<?> app = z3.mkApp(fd, array);
+        funcAppTranslation.put(buildFunctionLabel("length", new Expr<?>[] { array }), app);
+        return app;
+    }
+
     /**
      * Gets function declarations when an exact qualified name lookup fails. Tries to match by simple name and number of
      * parameters, preferring an exact qualified-name match if found among candidates; otherwise returns the first