René's URL Explorer Experiment

{"@context":"https://schema.org","@type":"DiscussionForumPosting","headline":"Typestate transition lost when state-changing call is stored in a boolean variable before the if","articleBody":"**Description**\nState change inside if has a different effect after the if\n\n**Minimal reproducer**\nClient Error:\n```java\n    float readAverage(Connection conn) throws SQLException {\n        Statement parentstmt = conn.createStatement();\n        ResultSet parentMessage =\n                parentstmt.executeQuery(\"SELECT SUM(IMPORTANCE) AS IMPAVG FROM MAIL\");\n        float avgsum = 0.0f;\n        boolean b = parentMessage.next();\n        if (b){\n            avgsum = parentMessage.getFloat(\"IMPAVG\");\n        }\n        return avgsum;\n    }\n```\nBut this way is correct:\n```java\n        float avgsum = 0.0f;\n        if (parentMessage.next()){\n            avgsum = parentMessage.getFloat(\"IMPAVG\");\n        }\n```\n\n\nWith the refinements:\n```java\n@StateSet({ \"onRow\", \"endRows\"})\n@ExternalRefinementsFor(\"java.sql.ResultSet\")\npublic interface ResultSetRefinements {\n\n    @StateRefinement(to = \"_ ? onRow(this) : endRows(this)\")\n    boolean next();\n\n\n    @StateRefinement(from = \"onRow(this)\")\n    float getFloat(String columnIndex);\n}\n```\n\n**Expected behavior**\nThis should not trigger an error as the getFloat is protetcted by already being `inRow()` but that is not happening.\n\n**Actual behavior**\n```\n[SMT] Verifying /Users/cgamboa/git/task-examples/liquidjava-tasks/src/main/java/com/example/so_clients/resultset8039233/ResultSetReadBeforeNext.java:23  on 'parentMessage.getFloat(\"IMPAVG\");'\n[SMT] \n[SMT]   #parentMessage_7 : ResultSet          #java.sql.ResultSet.next_6 ? state1(#parentMessage_7) == 0 : state1(#parentMessage_7) == 1\n[SMT]   #java.sql.ResultSet.next_6 : boolean  true\n[SMT]   #fresh_10 : boolean                   true\n[SMT]   ────────────────────────────────────────\n[SMT] state1(#parentMessage_7) == 0\n[SMT] Result: SAT (subtype fails) — counterexample:\n[SMT]     #java.sql.ResultSet.next_6 = false\n[SMT]     state1(#parentMessage_7) = 1\n```\n\n**Environment**\n- LiquidJava version / commit: #237 \n- Java version (`java -version`):\n- OS:\n","author":{"url":"https://github.com/CatarinaGamboa","@type":"Person","name":"CatarinaGamboa"},"datePublished":"2026-06-02T13:57:24.000Z","interactionStatistic":{"@type":"InteractionCounter","interactionType":"https://schema.org/CommentAction","userInteractionCount":0},"url":"https://github.com/241/liquidjava/issues/241"}