Misuse of @LowerBoundBottom

Consider the following code:

class tryit{
        void issue(int[] a, int[] b){
                int i;
                for(i = 0 ; i < b.length && i < a.length ; i ++);
                for( ; i < a.length ; i ++){
                        a[i] = 0;
                }
        }
}

Run it by: javac -processor index tryit.java

Output:

tryit.java:6: error: [array.access.unsafe.low] Potentially unsafe array access: the index could be negative.
                        a[i] = 0;
                          ^
  found   : @LowerBoundBottom int
  required: an integer >= 0 (@NonNegative or @Positive)
1 error

Which shouldn't be the case, clearly. However, when I annotate i as @NonNegative, the error is not issued.

Start by compiling the provided tryit.java reproducer with javac -processor index tryit.java, then compare it with the version where i is annotated @NonNegative. Investigate how the loop and @LowerBoundBottom result in the unsafe array-access diagnostic. Done means the unannotated code no longer reports a potentially negative index while the annotation case remains correct.