#include<mem.cvh>
$input int N;
$assume(N > 5);

int a[2*N];

int main() {
  $mem m = &a[0 .. N-1];
  
  $mem_havoc(m);
  
  $assert(a[N] == 0);
  $assert(a[N+1] == 0);
}