Difference in verification depending where the static method is place.

[wadoon]

Description

Consider the file Point3d.java. Method Point3d#test() is not verifiable, where as Use#m() is. Content-wise, they are identical.

public record Point3d(int x, int y, int z) {
    /*@ normal_behavior ensures true; requires true; */
    public static void test() {
        Point3d p = new Point3d(1, 2, 3);

        //boolean b= p.equals(p);
        // @assert b;

        //@ assert p.x() == 1;
        //@ assert p.y() == 2;
        //@ assert p.z() == 3;

        //@assert p.equals(p);

        Point3d q = new Point3d(p.x, p.y, p.z);
        //@assert p.equals(q);
        //@assert q.equals(p);
    }
}

class Use {
    /*@ normal_behavior ensures true; requires true; */
    public static void m() {
        Point3d p = new Point3d(1, 2, 3);

        //boolean b= p.equals(p);
        // @assert b;

        //@ assert p.x() == 1;
        //@ assert p.y() == 2;
        //@ assert p.z() == 3;

        //@assert p.equals(p);

        Point3d q = new Point3d(p.x, p.y, p.z);
        //@assert p.equals(q);
        //@assert q.equals(p);
    }
}

Reproducible

always

Steps to reproduce

Describe the steps needed to reproduce the issue.

1. Load the example above.
2. Prove Use#m() using auto
3. Try to prove Point3d#test()

---

• Commit: 4fc5ecc

[WolframPfeifer]

In the example above, both methods are static. Is the title of this PR or the example code wrong?

[WolframPfeifer]

I am confused now: Shouldn't the example be at least loadable after #3905 on the current RC for KeY 3.0? I thought there was a pipeline step that transforms records into normal classes?!

Edit: I got confused with the branches, and tried on prereleases/KeY-3.0.0-JP-rc instead of prereleases/KeY-3.0.0-rc, which is the correct RC branch and on which it loads as expected. Can we delete the former, as it is very easy to confuse?

[WolframPfeifer]

Now that the title is changed: I cannot reproduce this, as I am not able to prove any of the two variants.