Get Refinements needs to visit the variable first

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/ResultSetTests.java

@@ -62,4 +62,20 @@ float readAverage(Connection conn) throws SQLException {
             return 0.0f;
         }
     }
+
+    float readAverageStoredCondition(Connection conn) throws SQLException {
+        Statement parentstmt = conn.createStatement();
+        ResultSet parentMessage =
+                parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
+        // Regression for issue #241: next()'s result is stored in a boolean before the `if`.
+        // The transition (_ ? onRow : endRows) must still flow through `b`, so the guarded
+        // getFloat() is on a row (onRow) and verifies — exactly as the inline readAverage above.
+        boolean b = parentMessage.next();
+        if( b ) {
+            float avgsum = parentMessage.getFloat("IMPAVG");
+            return avgsum;
+        } else {
+            return 0.0f;
+        }
+    }
 }

liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/ResultSetTests.java

@@ -67,4 +67,29 @@ float readAverage(Connection conn) throws SQLException {
         float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
         return avgsum;
     }
+
+    // Issue #241 soundness: storing next()'s result in a boolean must NOT make getFloat()
+    // unconditionally legal. With no guard the state is `next ? onRow : endRows`, so onRow is
+    // not guaranteed and getFloat() must still be rejected.
+    float readAverageStoredNoGuard(Connection conn) throws SQLException {
+        Statement parentstmt = conn.createStatement();
+        ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
+        boolean b = parentMessage.next();
+        float avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
+        return avgsum;
+    }
+
+    // Issue #241 branch-sensitivity: legal in the then-branch (onRow), illegal in the else-branch (endRows).
+    float readAverageVarElse(Connection conn) throws SQLException {
+        Statement parentstmt = conn.createStatement();
+        ResultSet parentMessage = parentstmt.executeQuery("SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL");
+        float avgsum = 0.0f;
+        boolean b = parentMessage.next();
+        if (b) {
+            avgsum = parentMessage.getFloat("IMPAVG");
+        } else {
+            avgsum = parentMessage.getFloat("IMPAVG"); // State Refinement Error
+        }
+        return avgsum;
+    }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -321,6 +321,10 @@ private <T> boolean tryStaticFinalConstantRefinement(CtFieldRead<T> fieldRead) {
     public <T> void visitCtVariableRead(CtVariableRead<T> variableRead) {
         super.visitCtVariableRead(variableRead);
         CtVariable<T> varDecl = variableRead.getVariable().getDeclaration();
+        // Some CtVariableRead forms have no resolvable declaration (e.g. accesses to symbols outside the
+        // model); with no name there is no context entry to attach, so leave the metadata as-is.
+        if (varDecl == null)
+            return;
         getPutVariableMetadata(variableRead, varDecl.getSimpleName());
     }
 
@@ -538,8 +542,11 @@ private Predicate getAssignmentRefinement(String name, CtExpression<?> assignmen
     }
 
     private Predicate getExpressionRefinements(CtExpression<?> element) throws LJError {
-        if (element instanceof CtVariableRead<?>) {
-            // CtVariableRead<?> elemVar = (CtVariableRead<?>) element;
+        if (element instanceof CtFieldRead<?> fieldRead) {
+            visitCtFieldRead(fieldRead);
+            return getRefinement(element);
+        } else if (element instanceof CtVariableRead<?> varRead) {
+            visitCtVariableRead(varRead);
             return getRefinement(element);
         } else if (element instanceof CtBinaryOperator<?>) {
             CtBinaryOperator<?> binop = (CtBinaryOperator<?>) element;