int main(){
  int y;
  $havoc(&y);
  return 0;
}