After `s.contains(b)` returns true, `s.indexOf()` should have an `@IntRange` type

Consider the following code-

Command-

javac -processor signedness issue.java

Input-

import org.checkerframework.common.value.qual.*;
class issue {
    static final String s = "abcdefghijklmnopqrstuvwxyz";
    static void m1(String b) {
        if (s.contains(b)) {
            @IntRange(from=0, to=25) int temp = s.indexOf(b);
        }
    }
}

Output-

ex.java:6: error: [assignment.type.incompatible] incompatible types in assignment.
			@IntRange(from=0, to=25) int temp = s.indexOf(b);
			                                            ^
  found   : @UnknownVal int
  required: @IntRange(from=0, to=25) int
1 error

The error should not occur because if String s will contain String b then temp cannot be negative, therefore IntRange should satisfy this condition. I think the problem is that it is unable to detect the range of indexOf() otherwise this error would not occur.

Start with the provided issue.java example and run javac -processor signedness issue.java to reproduce the assignment error. Trace the signedness checker's handling of String.contains and String.indexOf, then add coverage showing that a successful contains check permits the nonnegative @IntRange assignment without an incompatible-type error.