source: CIVL/examples/mem/mem_tests/mem_union_widening_array.cvl

#include<mem.cvh>

int a[10];

int main() {
  $mem m = &a[0];
  
  m = $mem_union_widening(m, &a[1]);
  // only if the two indices connect, the default widening operator will
  // combine them precisely:
  $assert($mem_contains(m, &a[0 .. 1]));
  $assert(!$mem_contains(m, &a[2]));
  
  // otherwise, the default widening operator will result in the whole
  // array:
  m = $mem_union_widening(m, &a[3]);
  $assert($mem_contains(m, &a));

  m = &a[0 .. 2];
  m = $mem_union_widening(m, &a[1]);
  $assert($mem_contains(m, &a[0 .. 2]));
  $assert(!$mem_contains(m, &a));
}