import org.checkerframework.checker.index.qual.Positive;
import org.checkerframework.common.value.qual.*;

class MinLenFromPositive {

    void test(@Positive int x) {
        int @MinLen(1) [] y = new int[x];
        @IntRange(from = 1) int z = x;
        @Positive int q = x;
    }

    @SuppressWarnings("index")
    void foo(int x) {
        test(x);
    }

    void foo2(int x) {
        // :: error: (argument.type.incompatible)
        test(x);
    }

    void test_lub1(boolean flag, @Positive int x, @IntRange(from = 6, to = 25) int y) {
        int z;
        if (flag) {
            z = x;
        } else {
            z = y;
        }
        @Positive int q = z;
        @IntRange(from = 1) int w = z;
    }

    void test_lub2(boolean flag, @Positive int x, @IntRange(from = -1, to = 11) int y) {
        int z;
        if (flag) {
            z = x;
        } else {
            z = y;
        }
        // :: error: (assignment.type.incompatible)
        @Positive int q = z;
        @IntRange(from = -1) int w = z;
    }

    @Positive int id(@Positive int x) {
        return x;
    }

    void test_id(int param) {
        @Positive int x = id(5);
        @IntRange(from = 1) int y = id(5);

        int @MinLen(1) [] a = new int[id(100)];
        // :: error: (assignment.type.incompatible)
        int @MinLen(10) [] c = new int[id(100)];

        int q = id(10);

        if (param == q) {
            int @MinLen(1) [] d = new int[param];
        }
    }
}