int main() {
  int * ap;

  $havoc(&ap);
  if (1 > 0) {
    int x[100];

    $assume(x == ap);
    for (int i = 0; i < 99; i++)
      ap += 1;
  }
  $assert(*ap == 0);
}