`--rac`: "cannot find symbol" on `chars`/`modelString` in `Path.jml` postcondition

[ANogin]

[Caveat: Aided by Claude Code; I confirmed the specific findings, but not the underlying logic]

Reproducer

import java.nio.file.Path;
public class Foo { public void bar(Path p) {} }

$ openjml --rac Foo.java
[...]/specs/java/nio/file/Path.jml:97: error: cannot find symbol
    //@   ensures \result.chars == modelString;
                         ^
  symbol:   variable chars
  location: class String
[..]/specs/java/nio/file/Path.jml:97: error: cannot find symbol
    //@   ensures \result.chars == modelString;
                                   ^
  symbol:   variable modelString
  location: interface Path
2 errors

Observation

Both chars and modelString are declared //-RAC@ on Object.jml:

Specs/specs/java/lang/Object.jml

Lines 41 to 47 in 5cdfa1b

	// This \string represents the value that will be produced by toString()
	//-RAC@ model public instance \string modelString; in objectState;
	// This \string represents the value acucmulated by CharSequence and its derived classes,
	// and also by Appendable and its derived classes -- it would be nice if this could be the same
	// as modelString but it is possible for derived classes to have these be different values
	//-RAC@ model public instance \string chars; in objectState;

Object.jml's own toString() wraps its postcondition in /*-RAC@*/:

Specs/specs/java/lang/Object.jml

Lines 204 to 205 in 5cdfa1b

	/*-RAC@ public normal_behavior
	@ ensures \result.chars == modelString;

Path.jml's also clause uses plain //@ ensures instead:

Specs/specs/java/nio/file/Path.jml

Lines 96 to 97 in 5cdfa1b

	//@ also public normal_behavior
	//@ ensures \result.chars == modelString;