Typestate transition lost when state-changing call is stored in a boolean variable before the if

[CatarinaGamboa]

Description
State change inside if has a different effect after the if

Minimal reproducer
Client Error:

    float readAverage(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");
        }
        return avgsum;
    }

But this way is correct:

        float avgsum = 0.0f;
        if (parentMessage.next()){
            avgsum = parentMessage.getFloat("IMPAVG");
        }

With the refinements:

@StateSet({ "onRow", "endRows"})
@ExternalRefinementsFor("java.sql.ResultSet")
public interface ResultSetRefinements {

    @StateRefinement(to = "_ ? onRow(this) : endRows(this)")
    boolean next();


    @StateRefinement(from = "onRow(this)")
    float getFloat(String columnIndex);
}

Expected behavior
This should not trigger an error as the getFloat is protetcted by already being inRow() but that is not happening.

Actual behavior

[SMT] Verifying /Users/cgamboa/git/task-examples/liquidjava-tasks/src/main/java/com/example/so_clients/resultset8039233/ResultSetReadBeforeNext.java:23  on 'parentMessage.getFloat("IMPAVG");'
[SMT] 
[SMT]   #parentMessage_7 : ResultSet          #java.sql.ResultSet.next_6 ? state1(#parentMessage_7) == 0 : state1(#parentMessage_7) == 1
[SMT]   #java.sql.ResultSet.next_6 : boolean  true
[SMT]   #fresh_10 : boolean                   true
[SMT]   ────────────────────────────────────────
[SMT] state1(#parentMessage_7) == 0
[SMT] Result: SAT (subtype fails) — counterexample:
[SMT]     #java.sql.ResultSet.next_6 = false
[SMT]     state1(#parentMessage_7) = 1

Environment

• LiquidJava version / commit: Add Element Context to Exceptions #237
• Java version (java -version):
• OS: