Implement @ReturnsReceiver and make pre-/post-conditions (@EnsuresNonNull / @RequiresNonNull) understand it

I am getting some unexpected results using @EnsuresNonNull / @RequiresNonNull with a fluent API. This is with Checker Framework 2.8.0. Consider the following example:

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
public class Library {
    static class Example {
        @MonotonicNonNull String s;
        public Example() {}
        @EnsuresNonNull("this.s")
        public Example setS(String s1) {
            this.s = s1;
            return this;
        }
        @RequiresNonNull("this.s")
        public void print() {
            System.out.println(this.s.toString());
        }
    }
    static void withVars() {
        Example example = new Example();
        example.setS("hi");
        example.print();
    }
    static void fluent1() {
        Example example = new Example();
        example
            .setS("hi")
            .print();
    }
    static void fluent2() {
        (new Example())
            .setS("hi")
            .print();
    }
}

I would expect this code to typecheck with no errors. However, when running Nullness Checker I get the following error inside fluent1():

Library.java:43: error: [contracts.precondition.not.satisfied] example.setS("hi").print's precondition about 'example.setS("hi").s' is not satisfied
            .print();
                  ^
1 error

Adding an @Pure annotation to setS() does not fix the problem. Also, it is a bit surprising that fluent1() does not type check, but getting rid of the example local variable in fluent2() makes the code type check.

Start with the Nullness Checker handling of @EnsuresNonNull and @RequiresNonNull, then trace how the proposed @ReturnsReceiver annotation would affect fluent calls. Use the fluent1() and fluent2() examples as the behavioral checks; done means both examples typecheck without precondition errors.