#include<assert.h>
#include<civlc.cvh>

$input int n;
$input int m;
$assume(n>=1 && m>=1);
$input int A[n];
$input int B[n][m];

int f(int *x){
  return x[0]*2;
}

int main(){
  int a[n],b[n][m],c;
  $domain(2) dom=($domain(2)){0 .. n-1, 0 .. m-1};

  a=(int[n]) $lambda(int i) i*2;
  assert($forall(int k: 0 .. n-1) a[k]==k*2);
  a=(int[n]) $lambda(int i) A[i]*2;
  assert($forall(int i: 0 .. n-1) a[i]==A[i]*2);
  b=(int[n][m]) $lambda(int i, j) i+j;
  assert($forall(int i: 0 .. n-1; int j: 0 .. m-1) b[i][j]==i+j);
  b=(int[n][m]) $lambda(int i,j) B[i][j] * 5;
  assert($forall(int i: 0 .. n-1; int j: 0 .. m-1) b[i][j]==B[i][j]*5);
  c=f((int[n]) $lambda(int k) a[k]);
  assert(c==a[0]*2);
}