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

class BasicSubsequence {
    // :: error: not.final
    @HasSubsequence(subsequence = "this", from = "this.x", to = "this.y")
    int[] b;

    int x;
    int y;

    void test2(@NonNegative @LessThan("y + 1") int x1, int[] a) {
        x = x1;
        // :: error: to.not.ltel
        b = a;
    }

    void test3(@NonNegative @LessThan("y") int x1, int[] a) {
        x = x1;
        // :: error: to.not.ltel
        b = a;
    }

    void test4(@NonNegative int x1, int[] a) {
        x = x1;
        // :: error: from.gt.to :: error: to.not.ltel
        b = a;
    }

    void test5(@GTENegativeOne @LessThan("y + 1") int x1, int[] a) {
        x = x1;
        // :: error: from.not.nonnegative :: error: to.not.ltel
        b = a;
    }

    void test6(@GTENegativeOne int x1, int[] a) {
        x = x1;
        // :: error: from.not.nonnegative :: error: to.not.ltel :: error: from.gt.to
        b = a;
    }

    void test7(@IndexFor("this") @LessThan("y") int x1, @IndexOrHigh("this") int y1, int[] a) {
        x = x1;
        y = y1;
        // :: warning: which.subsequence
        b = a;
    }
}