Writing a field of a class declared later in the file crashes verification #308

Description

Writing a field of an object whose class is declared later in the file crashes verification ("mainRV" is null). Declaring the nested class before the method that writes the field makes it pass, so it depends only on declaration order. (Assigning this.field and writing fields of classes declared earlier already work on main.)

Minimal reproducer (no refinements needed)

public class Repro {
    private final Job job = new Job();
    public void send(int port) { job.port = port; }
    static class Job { int port; }
}

Expected

Correct! Passed Verification.

Actual

  on job.port = port; } 
  with Cannot invoke "liquidjava.processor.context.RefinedVariable.getSuperTypes()" because "mainRV" is null

Moving static class Job { int port; } above send gives Correct! Passed Verification.

Reproduced on main at 8816186 (liquidjava-verifier 0.0.35).

Context

Found while turning real open-source Java code into study examples for the error-message study. Real classes usually declare helper classes (runnables, DTOs) at the bottom; here a UDP client writes sendDataRunnable.address = address into a private static class SendDataRunnable declared further down, so the example cannot be verified at all.