Contracts.Precondition.Not.Satisfied error for `@RequiresNonNull("#1")` but not for `@NonNull` on formal parameter

I got the contracts.precondition.not.satisfied error while running the following code:
Link to the code.

import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

class A {
  
  @NonNull String message = "default string";
  
  @RequiresNonNull("#1")
  void setMessage(String message){
    this.message = message;
  }
  
  void main(){
    A object = new A();
    String mess = "random message";
    object.setMessage(mess.substring(0, mess.length() - 3));
  } 
}

class B {
  
  @NonNull String message = "default string";
  
  void setMessage(@NonNull String message){
    this.message = message;
  }
  
  void main(){
    B object = new B();
    String mess = "random message";
    object.setMessage(mess.substring(0, mess.length() - 3));
  } 
}

The exact error message follows :
I had used the Checker Framework Live Demo webpage to produce the error.

Error: [contracts.precondition.not.satisfied] the called method 'object.setMessage(mess.substring(0, mess.length() - 3))' has a precondition 'mess.substring(0, ?)' that is not satisfied

There is no error in the second version that removes @RequiresNonNull and uses @NonNull instead.

Start with the Checker Framework Live Demo reproduction in the issue and compare the two setMessage variants using @RequiresNonNull("#1") and @NonNull. Trace how the nullness checker interprets the mess.substring(0, mess.length() - 3) argument and the reported contracts.precondition.not.satisfied diagnostic. Done means the differing behavior is explained and the intended diagnostic behavior is established.