// Test case for issue 98: https://github.com/kelloggm/checker-framework/issues/98

import org.checkerframework.checker.index.qual.*;

public class SubtractingNonNegatives {
    public static void m4(int[] a, @IndexFor("#1") int i, @IndexFor("#1") int j) {
        int k = i;
        if (k >= j) {
            @IndexFor("a") int y = k;
        }
        for (k = i; k >= j; k -= j) {
            @IndexFor("a") int x = k;
        }
    }

    @SuppressWarnings("lowerbound")
    void test(int[] a, @Positive int y) {
        @LTLengthOf("a") int x = a.length - 1;
        @LTLengthOf(
                value = {"a", "a"},
                offset = {"0", "y"})
        int z = x - y;
        a[z + y] = 0;
    }

    @SuppressWarnings("lowerbound")
    void test2(int[] a, @Positive int y) {
        @LTLengthOf("a") int x = a.length - 1;
        int z = x - y;
        a[z + y] = 0;
    }
}