int main() {
  int N;
  int M;

  $havoc(&M);
  $havoc(&N);
  $assume(N > 0 && M > 0);

  int (*a)[M+2];
  int (*b)[M+2];
  int i, j;
  int c[N+2][M+2];
  int d[N+2][M+2];

  a = c;
  b = d;
  $havoc(&i);
  $havoc(&j);
  $assume(1 <= i && i <= N+1 && ($forall (int t : 1 .. i-1)  $forall (int x : 1 .. M)
				 b[t][x] == 0 ));
  $assume(i < N+1);
  i++;
  $assert(($forall (int t : 1 .. i-1)  $forall (int x : 1 .. M)
				 b[t][x] == 0));
}