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()
  {
  bool _J292, _x__J292;
  float x_3, _x_x_3;
  bool _J286, _x__J286;
  bool _EL_U_269, _x__EL_U_269;
  float x_5, _x_x_5;
  float x_0, _x_x_0;
  float x_4, _x_x_4;
  float x_6, _x_x_6;
  bool _EL_U_271, _x__EL_U_271;
  float x_2, _x_x_2;
  float x_7, _x_x_7;
  float x_1, _x_x_1;
  
    int __steps_to_fair = __VERIFIER_nondet_int();
    _J292 = __VERIFIER_nondet_bool();
    x_3 = __VERIFIER_nondet_float();
    _J286 = __VERIFIER_nondet_bool();
    _EL_U_269 = __VERIFIER_nondet_bool();
    x_5 = __VERIFIER_nondet_float();
    x_0 = __VERIFIER_nondet_float();
    x_4 = __VERIFIER_nondet_float();
    x_6 = __VERIFIER_nondet_float();
    _EL_U_271 = __VERIFIER_nondet_bool();
    x_2 = __VERIFIER_nondet_float();
    x_7 = __VERIFIER_nondet_float();
    x_1 = __VERIFIER_nondet_float();
  
    bool __ok = (1 && ((( !(( !((x_5 + (-1.0 * x_7)) <= 3.0)) && (_EL_U_271 || ( !(((x_4 + (-1.0 * x_5)) <= -3.0) || _EL_U_269))))) && ( !_J286)) && ( !_J292)));
    while (__steps_to_fair >= 0 && __ok) {
      if ((_J286 && _J292)) {
        __steps_to_fair = __VERIFIER_nondet_int();
      } else {
        __steps_to_fair--;
      }
      _x__J292 = __VERIFIER_nondet_bool();
      _x_x_3 = __VERIFIER_nondet_float();
      _x__J286 = __VERIFIER_nondet_bool();
      _x__EL_U_269 = __VERIFIER_nondet_bool();
      _x_x_5 = __VERIFIER_nondet_float();
      _x_x_0 = __VERIFIER_nondet_float();
      _x_x_4 = __VERIFIER_nondet_float();
      _x_x_6 = __VERIFIER_nondet_float();
      _x__EL_U_271 = __VERIFIER_nondet_bool();
      _x_x_2 = __VERIFIER_nondet_float();
      _x_x_7 = __VERIFIER_nondet_float();
      _x_x_1 = __VERIFIER_nondet_float();
  
      __ok = ((((((((((((x_7 + (-1.0 * _x_x_0)) <= -15.0) && (((x_6 + (-1.0 * _x_x_0)) <= -19.0) && (((x_3 + (-1.0 * _x_x_0)) <= -1.0) && ((x_5 + (-1.0 * _x_x_0)) <= -2.0)))) && (((x_7 + (-1.0 * _x_x_0)) == -15.0) || (((x_6 + (-1.0 * _x_x_0)) == -19.0) || (((x_3 + (-1.0 * _x_x_0)) == -1.0) || ((x_5 + (-1.0 * _x_x_0)) == -2.0))))) && ((((x_6 + (-1.0 * _x_x_1)) <= -4.0) && (((x_5 + (-1.0 * _x_x_1)) <= -6.0) && (((x_1 + (-1.0 * _x_x_1)) <= -1.0) && ((x_4 + (-1.0 * _x_x_1)) <= -16.0)))) && (((x_6 + (-1.0 * _x_x_1)) == -4.0) || (((x_5 + (-1.0 * _x_x_1)) == -6.0) || (((x_1 + (-1.0 * _x_x_1)) == -1.0) || ((x_4 + (-1.0 * _x_x_1)) == -16.0)))))) && ((((x_6 + (-1.0 * _x_x_2)) <= -15.0) && (((x_4 + (-1.0 * _x_x_2)) <= -10.0) && (((x_0 + (-1.0 * _x_x_2)) <= -15.0) && ((x_3 + (-1.0 * _x_x_2)) <= -6.0)))) && (((x_6 + (-1.0 * _x_x_2)) == -15.0) || (((x_4 + (-1.0 * _x_x_2)) == -10.0) || (((x_0 + (-1.0 * _x_x_2)) == -15.0) || ((x_3 + (-1.0 * _x_x_2)) == -6.0)))))) && ((((x_7 + (-1.0 * _x_x_3)) <= -18.0) && (((x_5 + (-1.0 * _x_x_3)) <= -3.0) && (((x_3 + (-1.0 * _x_x_3)) <= -17.0) && ((x_4 + (-1.0 * _x_x_3)) <= -13.0)))) && (((x_7 + (-1.0 * _x_x_3)) == -18.0) || (((x_5 + (-1.0 * _x_x_3)) == -3.0) || (((x_3 + (-1.0 * _x_x_3)) == -17.0) || ((x_4 + (-1.0 * _x_x_3)) == -13.0)))))) && ((((x_7 + (-1.0 * _x_x_4)) <= -2.0) && (((x_3 + (-1.0 * _x_x_4)) <= -18.0) && (((x_0 + (-1.0 * _x_x_4)) <= -11.0) && ((x_2 + (-1.0 * _x_x_4)) <= -12.0)))) && (((x_7 + (-1.0 * _x_x_4)) == -2.0) || (((x_3 + (-1.0 * _x_x_4)) == -18.0) || (((x_0 + (-1.0 * _x_x_4)) == -11.0) || ((x_2 + (-1.0 * _x_x_4)) == -12.0)))))) && ((((x_5 + (-1.0 * _x_x_5)) <= -15.0) && (((x_4 + (-1.0 * _x_x_5)) <= -20.0) && (((x_1 + (-1.0 * _x_x_5)) <= -8.0) && ((x_3 + (-1.0 * _x_x_5)) <= -10.0)))) && (((x_5 + (-1.0 * _x_x_5)) == -15.0) || (((x_4 + (-1.0 * _x_x_5)) == -20.0) || (((x_1 + (-1.0 * _x_x_5)) == -8.0) || ((x_3 + (-1.0 * _x_x_5)) == -10.0)))))) && ((((x_7 + (-1.0 * _x_x_6)) <= -11.0) && (((x_6 + (-1.0 * _x_x_6)) <= -9.0) && (((x_3 + (-1.0 * _x_x_6)) <= -11.0) && ((x_4 + (-1.0 * _x_x_6)) <= -9.0)))) && (((x_7 + (-1.0 * _x_x_6)) == -11.0) || (((x_6 + (-1.0 * _x_x_6)) == -9.0) || (((x_3 + (-1.0 * _x_x_6)) == -11.0) || ((x_4 + (-1.0 * _x_x_6)) == -9.0)))))) && ((((x_7 + (-1.0 * _x_x_7)) <= -10.0) && (((x_6 + (-1.0 * _x_x_7)) <= -20.0) && (((x_0 + (-1.0 * _x_x_7)) <= -20.0) && ((x_3 + (-1.0 * _x_x_7)) <= -8.0)))) && (((x_7 + (-1.0 * _x_x_7)) == -10.0) || (((x_6 + (-1.0 * _x_x_7)) == -20.0) || (((x_0 + (-1.0 * _x_x_7)) == -20.0) || ((x_3 + (-1.0 * _x_x_7)) == -8.0)))))) && ((((_EL_U_269 == (_x__EL_U_269 || ((_x_x_4 + (-1.0 * _x_x_5)) <= -3.0))) && (_EL_U_271 == (_x__EL_U_271 || ( !(_x__EL_U_269 || ((_x_x_4 + (-1.0 * _x_x_5)) <= -3.0)))))) && (_x__J286 == (( !(_J286 && _J292)) && ((_J286 && _J292) || ((((x_4 + (-1.0 * x_5)) <= -3.0) || ( !(((x_4 + (-1.0 * x_5)) <= -3.0) || _EL_U_269))) || _J286))))) && (_x__J292 == (( !(_J286 && _J292)) && ((_J286 && _J292) || ((( !(((x_4 + (-1.0 * x_5)) <= -3.0) || _EL_U_269)) || ( !(_EL_U_271 || ( !(((x_4 + (-1.0 * x_5)) <= -3.0) || _EL_U_269))))) || _J292))))));
      _J292 = _x__J292;
      x_3 = _x_x_3;
      _J286 = _x__J286;
      _EL_U_269 = _x__EL_U_269;
      x_5 = _x_x_5;
      x_0 = _x_x_0;
      x_4 = _x_x_4;
      x_6 = _x_x_6;
      _EL_U_271 = _x__EL_U_271;
      x_2 = _x_x_2;
      x_7 = _x_x_7;
      x_1 = _x_x_1;
  
    }
  }
  