Refinements on fields of nested classes depend on declaration order and on field names. Real code often puts helper classes (runnables, DTOs) at the bottom of the file, so this comes up when verifying real-world examples (see #308, fixed by #314 for field writes).
The root cause is that fields are registered only in the second pass, in source order. They are stored under a name-only key (this#<name>), and the variable context is reset whenever any class is entered, nested classes included.
Sub-issues track the specific cases:
Refinements on fields of nested classes depend on declaration order and on field names. Real code often puts helper classes (runnables, DTOs) at the bottom of the file, so this comes up when verifying real-world examples (see #308, fixed by #314 for field writes).
The root cause is that fields are registered only in the second pass, in source order. They are stored under a name-only key (
this#<name>), and the variable context is reset whenever any class is entered, nested classes included.Sub-issues track the specific cases: