extern void __VERIFIER_error() __attribute__ ((__noreturn__));
extern void __VERIFIER_assume(int);
extern int __VERIFIER_nondet_int();

int main( ) {

  int input = __VERIFIER_nondet_int();

  if (input < 0) {
    __VERIFIER_error();
  } 

}