source: CIVL/examples/experimental/multInLoopCond.cvl@ d1b9862

$input int N;
$input int M;
$assume N > 0 && N < 3;
$assume M > 0 && M < 3;

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