GeezerVison

Description

This PR makes constructors preserve state refinements when an object is assigned directly to a class field.
Field initializers were visited but their refinement metadata was not transferred to the field’s symbolic instance.

Example

public class Test {

    private final Obj obj = new Obj();

    public void test() {
        obj.foo(); // reports state refinement error but should pass
    }
}

@Ghost("boolean ready")
class Obj {

    @StateRefinement(to = "ready(this)")
    Obj() {}

    @StateRefinement(from = "ready(this)")
    void foo() {}
}

Related Issue

None.

Type of change

• Bug fix
• New feature
• Documentation update
• Code refactoring

Checklist

• Added/updated tests under liquidjava-example/src/main/java/testSuite/ (Correct* / Error*)
• mvn test passes locally
• Updated docs/README if behavior or API changed