From 4cee75f33f88f055a62afd6e0da19b8eb2dfde22 Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com>
Date: Tue, 6 Oct 2026 20:22:58 +0100
Subject: [PATCH] Support length on arrays of any element type

Fixes #355. The builtin length was declared for int[] only, so .length of
any other array (String[], Object[], ...) in the context made every Z3 query
fail with a sort mismatch. length now gets one overload per array sort,
declared on first use.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../testSuite/CorrectStringArrayLength.java   | 20 +++++++++++++++++++
 .../testSuite/ErrorStringArrayLength.java     | 11 ++++++++++
 .../java/liquidjava/smt/TranslatorToZ3.java   | 17 ++++++++++++++++
 3 files changed, 48 insertions(+)
 create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectStringArrayLength.java
 create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStringArrayLength.java

diff --git a/liquidjava-example/src/main/java/testSuite/CorrectStringArrayLength.java b/liquidjava-example/src/main/java/testSuite/CorrectStringArrayLength.java
new file mode 100644
index 00000000..bd606285
--- /dev/null
+++ b/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;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStringArrayLength.java b/liquidjava-example/src/main/java/testSuite/ErrorStringArrayLength.java
new file mode 100644
index 00000000..dae416b7
--- /dev/null
+++ b/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
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
index ab4adfff..ac3eadd4 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
+++ b/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