source: CIVL/examples/mem/mem_tests/mem_no_intersect_array2d.cvl@ afc300c

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

$input int N;
$assume(N > 10);
int a[2*N][2*N];

int main() {

  $mem m = ($mem)&a[N .. 2*N-1][N .. 2*N-1];
  $mem n = ($mem)&a[5 .. 10][N .. 2*N-1];
  $mem out0, out1;
  _Bool noOverlap;

  noOverlap = $mem_no_intersect(m, n, &out0, &out1);
  $assert(noOverlap);
}