// Test case for issue #4248: https://github.com/typetools/checker-framework/issues/4248.
// This test exposed a crash in the original version of the fix.

import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.checker.index.qual.Positive;
import org.checkerframework.framework.qual.DefaultQualifier;

class DefaultForEach {

  @DefaultQualifier(NonNegative.class)
  static int[] foo() {
    throw new RuntimeException();
  }

  void bar() {
    for (Integer p : foo()) {
      // :: error: assignment
      @Positive int x = p;
      @NonNegative int y = p;
    }
  }
}