#include<mem.cvh>

$input int N,M;
$assume(6 <= N && N <= 10);
$assume(N <= M && M <= 2*N);
int a[N][M];

int main() {
  $mem m = &a[0 .. N-1][0 .. M-1];
  $mem m2 = &a[N-5 .. N-2][2 .. M-4];
  m = $mem_diff(m, m2);
  $mem m3 = &a[0..N-6][0..M-1];
  m3 = $mem_union(m3, &a[N-1..N-1][0..M-1]);
  m3 = $mem_union(m3, &a[0..N-1][0..1]);
  m3 = $mem_union(m3, &a[0..N-1][M-3..M-1]);
  $assert($mem_contains(m, m3));
}