#pragma CIVL ACSL
$input int N;
$assume(0 < N);
int a[N];

int main() {
  /*@ loop assigns a[0..N-1];
    @ focus F+1 | a[F];
    @*/
  for (int i = 1; i <= N; i++) {
    a[i-1] = 0;
  }

  
  //@ focus F;
  $assert($forall(int i:0..N-1) a[i] == 0);
}