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

/* An example shows how $pointer_realloc works. */
$input int N;
$input int M;
$assume(N > 4 && M > N + 2);
int main() {
  int * p = (int *)malloc(sizeof(int) * N);
  int a = p[1];  

  $pointer_realloc(p, sizeof(int) * M);

  $assert(p[1] == a);
  free(p);
  return 0;
}