#include <mem.cvh>
$input int N, n;
$assume(N > n && n > 5);

int main() {
  int x, y, z;
  double a[10], b[10][10];
  float c[N], d[2*N][2*N];
  
  $write_set_push();
  x = 0;
  y = 0;
  a[3] = 0;
  b[1][3] = 0;
  c[n] = 0;
  d[n*2][n*2] = 0;
  
  $mem m = $write_set_pop();
  $mem m2 = $mem_empty();

  m2 = $mem_union(m, &x);
  m2 = $mem_union(m, &y);
  m2 = $mem_union(m, &a[3]);
  m2 = $mem_union(m, &b[1][3]);
  m2 = $mem_union(m, &c[n]);
  m2 = $mem_union(m, &d[n*2][n*2]);
  $assert($mem_contains(m, m2));
  $assert($mem_contains(m, &z));
  return 0;
}