text: extern float __VERIFIER_nondet_float(void);
  extern int __VERIFIER_nondet_int(void);
  typedef enum {false, true} bool;
  bool __VERIFIER_nondet_bool(void) {
    return __VERIFIER_nondet_int() != 0;
  }
  
  int main()
  {
  float x_2, _x_x_2;
  bool _J130, _x__J130;
  bool _J124, _x__J124;
  bool _J118, _x__J118;
  bool _EL_X_86, _x__EL_X_86;
  bool _EL_U_92, _x__EL_U_92;
  float x_1, _x_x_1;
  bool _EL_U_94, _x__EL_U_94;
  bool _EL_U_96, _x__EL_U_96;
  float x_0, _x_x_0;
  float x_3, _x_x_3;
  
    int __steps_to_fair = __VERIFIER_nondet_int();
    x_2 = __VERIFIER_nondet_float();
    _J130 = __VERIFIER_nondet_bool();
    _J124 = __VERIFIER_nondet_bool();
    _J118 = __VERIFIER_nondet_bool();
    _EL_X_86 = __VERIFIER_nondet_bool();
    _EL_U_92 = __VERIFIER_nondet_bool();
    x_1 = __VERIFIER_nondet_float();
    _EL_U_94 = __VERIFIER_nondet_bool();
    _EL_U_96 = __VERIFIER_nondet_bool();
    x_0 = __VERIFIER_nondet_float();
    x_3 = __VERIFIER_nondet_float();
  
    bool __ok = (1 && (((( !(_EL_U_96 || ( !(_EL_U_94 || ( !(_EL_U_92 || ( !_EL_X_86))))))) && ( !_J118)) && ( !_J124)) && ( !_J130)));
    while (__steps_to_fair >= 0 && __ok) {
      if (((_J118 && _J124) && _J130)) {
        __steps_to_fair = __VERIFIER_nondet_int();
      } else {
        __steps_to_fair--;
      }
      _x_x_2 = __VERIFIER_nondet_float();
      _x__J130 = __VERIFIER_nondet_bool();
      _x__J124 = __VERIFIER_nondet_bool();
      _x__J118 = __VERIFIER_nondet_bool();
      _x__EL_X_86 = __VERIFIER_nondet_bool();
      _x__EL_U_92 = __VERIFIER_nondet_bool();
      _x_x_1 = __VERIFIER_nondet_float();
      _x__EL_U_94 = __VERIFIER_nondet_bool();
      _x__EL_U_96 = __VERIFIER_nondet_bool();
      _x_x_0 = __VERIFIER_nondet_float();
      _x_x_3 = __VERIFIER_nondet_float();
  
      __ok = ((((((((x_2 + (-1.0 * _x_x_0)) <= -18.0) && ((x_3 + (-1.0 * _x_x_0)) <= -10.0)) && (((x_2 + (-1.0 * _x_x_0)) == -18.0) || ((x_3 + (-1.0 * _x_x_0)) == -10.0))) && ((((x_0 + (-1.0 * _x_x_1)) <= -3.0) && ((x_3 + (-1.0 * _x_x_1)) <= -13.0)) && (((x_0 + (-1.0 * _x_x_1)) == -3.0) || ((x_3 + (-1.0 * _x_x_1)) == -13.0)))) && ((((x_0 + (-1.0 * _x_x_2)) <= -15.0) && ((x_1 + (-1.0 * _x_x_2)) <= -20.0)) && (((x_0 + (-1.0 * _x_x_2)) == -15.0) || ((x_1 + (-1.0 * _x_x_2)) == -20.0)))) && ((((x_2 + (-1.0 * _x_x_3)) <= -3.0) && ((x_3 + (-1.0 * _x_x_3)) <= -1.0)) && (((x_2 + (-1.0 * _x_x_3)) == -3.0) || ((x_3 + (-1.0 * _x_x_3)) == -1.0)))) && (((((_EL_U_96 == (_x__EL_U_96 || ( !(_x__EL_U_94 || ( !(_x__EL_U_92 || ( !_x__EL_X_86))))))) && ((_EL_U_94 == (_x__EL_U_94 || ( !(_x__EL_U_92 || ( !_x__EL_X_86))))) && ((_EL_X_86 == ((_x_x_0 + (-1.0 * _x_x_2)) <= 5.0)) && (_EL_U_92 == (_x__EL_U_92 || ( !_x__EL_X_86)))))) && (_x__J118 == (( !((_J118 && _J124) && _J130)) && (((_J118 && _J124) && _J130) || ((( !_EL_X_86) || ( !(_EL_U_92 || ( !_EL_X_86)))) || _J118))))) && (_x__J124 == (( !((_J118 && _J124) && _J130)) && (((_J118 && _J124) && _J130) || ((( !(_EL_U_92 || ( !_EL_X_86))) || ( !(_EL_U_94 || ( !(_EL_U_92 || ( !_EL_X_86)))))) || _J124))))) && (_x__J130 == (( !((_J118 && _J124) && _J130)) && (((_J118 && _J124) && _J130) || ((( !(_EL_U_94 || ( !(_EL_U_92 || ( !_EL_X_86))))) || ( !(_EL_U_96 || ( !(_EL_U_94 || ( !(_EL_U_92 || ( !_EL_X_86)))))))) || _J130))))));
      x_2 = _x_x_2;
      _J130 = _x__J130;
      _J124 = _x__J124;
      _J118 = _x__J118;
      _EL_X_86 = _x__EL_X_86;
      _EL_U_92 = _x__EL_U_92;
      x_1 = _x_x_1;
      _EL_U_94 = _x__EL_U_94;
      _EL_U_96 = _x__EL_U_96;
      x_0 = _x_x_0;
      x_3 = _x_x_3;
  
    }
  }
  