$input int N;
$assume(N > 0);
$input int M;
$assume(0 < M && M < N);

#pragma CIVL ACSL

int main() {  
  int b[N];
  
  /*@ loop invariant 0 <= i && i <= N;
    @ loop invariant \forall int i1; 0 <= i1 && i1 < (i<=M?i:M) ==> b[i1] == 0;
    @ loop invariant \forall int i1; M < i1 && i1 < i ==> b[i1] == 1;
    @ loop assigns i, b[0 .. M-1], b[M .. N-1];
    @*/
  for (int i = 0; i < N; i++) {
    if (i < M) b[i] = 0;
    else if (i > M) b[i] = 1;
  }
}