/* Commandline execution:
 *		civl verify multInLoopCond.cvl
 * */
$input int N;
$input int M;
$assume N > 0 && N < 3;
$assume M > 0 && M < 3;
$assume N*M<=4;

void main() {
  int k = M*N;
  int a[k];
  
  for (int i = 0; i < k; i++) {
    a[i] = i;
  }
}