#include<mem.cvh>

$input int N;
$assume(2 <= N && N <= 6);

typedef struct {
  int x[10];
} A;

int main() {
  A a[10];
  $mem m = &a[0 .. 9].x[0 .. 9];
  $mem m2 = &a[N-1 .. N+3].x[N-2 .. N+2];
  m = $mem_diff(m, m2);
  $mem m3 = &a[0..N-2].x[0..9];
  m3 = $mem_union(m3, &a[N+4..9].x[0..9]);
  m3 = $mem_union(m3, &a[0..9].x[0..N-3]);
  m3 = $mem_union(m3, &a[0..9].x[N+3..9]);
  $assert($mem_contains(m, m3));
}