source: CIVL/examples/mem/mem_tests/mem_no_intersect_array2d-bad.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 .. N + 5][N .. N + 5];
  $mem out0, out1;
  _Bool noOverlap;

  noOverlap = $mem_no_intersect(m, n, &out0, &out1);
  $assert(noOverlap, "\"%p\" and \"%p\" may intersect \n", out0, out1);
}