#include<mem.cvh>
#include<stdlib.h>

$input int N;
$assume(N > 5);

struct T {
  int a[2 * N];
  double b[2 * N][2 * N];
  struct T * t;
};

int main() {
  struct T t;

  $havoc(&t);

  struct T old_t = t;
  
  $mem m = &t.a[0 .. N-1];
  
  m = $mem_union(m, &t.b[0 .. N-1][N .. 2*N-1]);
  $mem_havoc(m);
  $assert($forall (int i : 0 .. N-1) 
	  $forall (int j : N .. 2*N-1)
	  t.a[j] == old_t.a[j] &&
	  t.b[j][i] == old_t.b[i][j] 
	  );
  free(t.t);
}