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

public class SameLenManyArrays {
  void transfer1(int @SameLen("#2") [] a, int[] b) {
    int[] c = new int[a.length];
    for (int i = 0; i < c.length; i++) { // i's type is @LTL("c")
      b[i] = 1;
      int @SameLen({"a", "b", "c"}) [] d = c;
    }
  }

  void transfer2(int @SameLen("#2") [] a, int[] b) {
    for (int i = 0; i < b.length; i++) { // i's type is @LTL("b")
      a[i] = 1;
    }
  }

  void transfer3(int @SameLen("#2") [] a, int[] b, int[] c) {
    if (a.length == c.length) {
      for (int i = 0; i < c.length; i++) { // i's type is @LTL("c")
        b[i] = 1;
        int @SameLen({"a", "b", "c"}) [] d = c;
      }
    }
  }

  void transfer4(int[] a, int[] b, int[] c) {
    if (b.length == c.length) {
      if (a.length == b.length) {
        for (int i = 0; i < c.length; i++) { // i's type is @LTL("c")
          a[i] = 1;
          int @SameLen({"a", "b", "c"}) [] d = c;
        }
      }
    }
  }

  void transfer5(int[] a, int[] b, int[] c, int[] d) {
    if (a.length == b.length && b.length == c.length) {
      int[] x = a;
      int[] y = x;
      int index = x.length - 1;
      if (index > 0) {
        f(a[index]);
        f(b[index]);
        f(c[index]);
        f(x[index]);
        f(y[index]);
      }
    }
  }

  @Pure
  void f(Object o) {}
}