#include <civlc.cvh>
/* 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;
  }
}