int main(){
  int x;

  while(1){
    $havoc(&x);
    $assume(x>0);
  }
}