int main() {
  int * ap;
  int x[100];
  
  $havoc(&ap);
  $assume(x == ap);
  for (int i = 0; i < 99; i++)
    ap += 1;
  $assert((*ap) == x[99]);
}