// Test case for https://github.com/kelloggm/checker-framework/issues/158
// It is easy to see that:
//   * i is an index for intermediate
//   * length <= i (or, at least length <= i+1)
// but I don't see how to verify that length is an index for intermediate.

// @skip-test

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

public class VarLteVar {

  /** Returns an array that is equivalent to the set difference of seq1 and seq2. */
  public static boolean[] setDiff(boolean[] seq1, boolean[] seq2) {
    boolean[] intermediate = new boolean[seq1.length];
    int length = 0;
    for (int i = 0; i < seq1.length; i++) {
      if (!memberOf(seq1[i], seq2)) {
        intermediate[length++] = seq1[i];
      }
    }
    return subarray(intermediate, 0, length);
  }

  public static boolean memberOf(boolean elt, boolean[] arr) {
    for (int i = 0; i < arr.length; i++) {
      if (arr[i] == elt) {
        return true;
      }
    }
    return false;
  }

  @SuppressWarnings("index") // not relevant to this test case
  public static boolean[] subarray(
      boolean[] a, @IndexOrHigh("#1") int startindex, @IndexOrHigh("#1") int length) {
    boolean[] result = new boolean[length];
    System.arraycopy(a, startindex, result, 0, length);
    return result;
  }
}