extern void __VERIFIER_error() __attribute__ ((__noreturn__));



int main()
{
 if (2+2 == 5){
  ERROR: __VERIFIER_error();
 }
 return 0;
}