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

int main() {

  int x = 0;
  /*@ loop invariant x == i;
    @ loop assigns a[0..N-1],x;
    @ focus F+{-1..1} | a[F-1..F+1];
    @*/
  for (int i = 0; i < N; i++) {
    a[i] = i + x;
    x = x+1;
  }
  
  //@ focus F;
  $assert($forall(int i:1..N-2) a[i-1] == 2*(i-1) && a[i] == 2*i && a[i+1] == 2*(i+1));
}