Description

CatarinaGamboa

opened on Oct 6, 2026

Issue body actions

Impact: correct code is rejected. It blocks 1 of the 48 real-code examples we built (bugs mined from open-source Java).

Description

Code with no refinements at all gets Syntax Error: Invalid refinement expression, expected a logical predicate on grid[i].length; grid.length is fine.

Minimal reproducer

public class Repro {
    static double sum(double[][] grid) {
        double total = 0;
        for (int i = 0; i < grid.length; i++) {
            for (int j = 0; j < grid[i].length; j++) {
                total += grid[i][j];
            }
        }
        return total;
    }

    public static void main(String[] args) {
        System.out.println(sum(new double[][] {{1, 2}, {3}}));
    }
}

Expected

Correct! Passed Verification. The expression is ordinary Java; at worst an unconstrained int.

Actual

Syntax Error: Invalid refinement expression, expected a logical predicate
3 |         double total = 0;
4 |         for (int i = 0; i < grid.length; i++) {
5 |             for (int j = 0; j < grid[i].length; j++) {
  |                                 ^^^^^^^^^^^^^^
6 |                 total += grid[i][j];
7 |             }
Repro.java:5

Reproduced on main at 0472025 (liquidjava-verifier 0.0.35); also on fbfb4e2 and 0.0.33 in the original form.

Context

Found while turning bugs mined from real open-source Java (fixed upstream or still present) into study examples for the error-message study.

Activity

1. CatarinaGamboa

   added

   bugSomething isn't workingSomething isn't working

   on Oct 6, 2026
2. CatarinaGamboa commented on Oct 13, 2026

   

   CatarinaGamboa

   on Oct 13, 2026

   CollaboratorAuthor

   More actions

   More forms, on main at ad055b4: .length on any array that is not a plain local seems to give the same false error, e.g. a field accessed through this:

   public class Repro {
       private String[] handlers = new String[0];
   
       int count() {
           int n = 0;
           for (int i = 0; i < this.handlers.length; i++) {
               n++;
           }
           return n;
       }
   }

   Syntax Error: Invalid refinement expression, expected a logical predicate
   6 |         for (int i = 0; i < this.handlers.length; i++) {
     |                             ^^^^^^^^^^^^^^^^^^^^
   

   (names().length on a call result passes in this small case.)

   Real files from the 53 originals of our study (each file verified on its own, so the project's other classes are not on the classpath):

   • iis.readFully(data[i], 0, data[i].length); — pacsbrasil/dcm4che2 (file) (and the same code in fenyuzhe/protoss-toolkit (file))
   • for ( int j = 0; j < embeddings[i].length; j++ ) { — darrenfoong/depnn (file)
   • if ((names[0].length == 0 || matches[0]) && ... and p.define().length > 0 (p an annotation of a class not on the classpath) — larael/javacpp (file)
   • for (int i = 0; i < this.errorHandlers.length; i++) { — storset/vtk.test (file)

   Related: the array-write index form (a[k++] = x) is a separate path: #397.
3. CatarinaGamboa

   added a commit that references this issue on Oct 29, 2026

   Fix crashes on unresolved types and on empty for bodies (#432)

   6f0239d

Issue actions