int nondet() { int a; return a; }
_Bool nondet_bool() { _Bool a; return a; }
int foo (int A, int B, int C) {
 goto loc_evalrealheapsortstep1start;

 loc_evalrealheapsortstep1bb2in:
 {
   if (nondet_bool()) {
    int C_ = -1;
    if (1 + C == 0) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int C_ = -1 + Y_0;
    if (1 + C == 0 && 1 + 2 * Y_0 >= 0 && 0 >= 2 * Y_0 && Y_0 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int C_ = -1;
    if (1 + C == 0 && 1 + 2 * Y_0 >= 0 && 0 >= 2 * Y_0 && Y_0 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1 + Y_0;
    if (1 + C == 0 && 1 + 2 * Y_0 >= 0 && 0 >= 2 * Y_0 && Y_0 >= 0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int C_ = -1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_1 = nondet();
    int Y_0 = nondet();
    int C_ = -1 + Y_1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= Y_0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 + C >= 2 * Y_1 && 2 * Y_1 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 0 >= Y_1 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int C_ = -1;
    if (1 + C == 0 && 1 + 2 * Y_0 >= 0 && 0 >= 2 * Y_0 && Y_0 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1 + Y_0;
    if (1 + C == 0 && 1 + 2 * Y_0 >= 0 && 0 >= 2 * Y_0 && Y_0 >= 0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1;
    if (1 + C == 0 && 1 + 2 * Y_0 >= 0 && 0 >= 2 * Y_0 && Y_0 >= 0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int Y_2 = nondet();
    int C_ = -1 + Y_0;
    if (2 * Y_0 >= C && 1 + C >= 2 * Y_0 && Y_0 >= 0 && 2 * Y_1 >= C && 1 + C >= 2 * Y_1 && Y_1 >= 0 && 2 * Y_2 >= C && 1 + C >= 2 * Y_2 && Y_2 >= 0 && C >= 0) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int Y_2 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 0 >= Y_0 && 0 >= 2 + C && 2 * Y_1 >= C && 1 + C >= 2 * Y_1 && Y_1 >= 0 && 2 * Y_2 >= C && 1 + C >= 2 * Y_2 && Y_2 >= 0 && C >= 0) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_1 = nondet();
    int Y_0 = nondet();
    int Y_2 = nondet();
    int C_ = -1 + Y_1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 * Y_1 >= C && 1 + C >= 2 * Y_1 && Y_1 >= 0 && 0 >= Y_0 && 0 >= 2 + C && 2 * Y_2 >= C && 1 + C >= 2 * Y_2 && Y_2 >= 0 && C >= 0) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int Y_2 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 + C >= 2 * Y_1 && 2 * Y_1 >= 1 + C && 0 >= Y_0 && 0 >= Y_1 && 0 >= 2 + C && 2 * Y_2 >= C && 1 + C >= 2 * Y_2 && Y_2 >= 0 && C >= 0) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int C_ = -1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_1 = nondet();
    int Y_0 = nondet();
    int C_ = -1 + Y_1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= Y_0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 + C >= 2 * Y_1 && 2 * Y_1 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 0 >= Y_1 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 1 + C == 0 && 1 + 2 * Y_1 >= 0 && 0 >= 2 * Y_1 && Y_1 >= 0 && 0 >= Y_0 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_1 = nondet();
    int Y_0 = nondet();
    int Y_2 = nondet();
    int C_ = -1 + Y_1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 * Y_1 >= C && 1 + C >= 2 * Y_1 && Y_1 >= 0 && 2 * Y_2 >= C && 1 + C >= 2 * Y_2 && Y_2 >= 0 && C >= 0 && 0 >= Y_0 && 0 >= 2 + C) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int Y_2 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 + C >= 2 * Y_1 && 2 * Y_1 >= 1 + C && 0 >= Y_0 && 2 * Y_2 >= C && 1 + C >= 2 * Y_2 && Y_2 >= 0 && C >= 0 && 0 >= Y_1 && 0 >= 2 + C) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 + C >= 2 * Y_1 && 2 * Y_1 >= 1 + C && 1 + C == 0 && 0 >= Y_0 && 0 >= Y_1 && 0 >= 1) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_2 = nondet();
    int Y_0 = nondet();
    int Y_1 = nondet();
    int C_ = -1 + Y_2;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 + C >= 2 * Y_1 && 2 * Y_1 >= 1 + C && 2 * Y_2 >= C && 1 + C >= 2 * Y_2 && Y_2 >= 0 && C >= 0 && 0 >= Y_0 && 0 >= Y_1 && 0 >= 2 + C) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    int Y_1 = nondet();
    int Y_2 = nondet();
    int C_ = -1 + Y_0;
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 2 + C >= 2 * Y_1 && 2 * Y_1 >= 1 + C && 2 + C >= 2 * Y_2 && 2 * Y_2 >= 1 + C && 0 >= Y_0 && 0 >= Y_1 && 0 >= Y_2 && 0 >= 2 + C) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
  goto end;
 }
 loc_evalrealheapsortstep1bb3in:
 {
   if (nondet_bool()) {
    if (0 >= C) {
     goto loc_evalrealheapsortstep1bb5in;
    }
   }
   if (nondet_bool()) {
    if (C >= 1) {
     goto loc_evalrealheapsortstep1bb4in;
    }
   }
  goto end;
 }
 loc_evalrealheapsortstep1bb4in:
 {
   if (nondet_bool()) {
    if (1 + C == 0) {
     goto loc_evalrealheapsortstep1bb2in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    if (2 * Y_0 >= C && 1 + C >= 2 * Y_0 && Y_0 >= 0 && C >= 0) {
     goto loc_evalrealheapsortstep1bb2in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 0 >= Y_0 && 0 >= 2 + C) {
     goto loc_evalrealheapsortstep1bb2in;
    }
   }
   if (nondet_bool()) {
    if (1 + C == 0) {
     goto loc_evalrealheapsortstep1bb5in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    if (2 * Y_0 >= C && 1 + C >= 2 * Y_0 && Y_0 >= 0 && C >= 0) {
     goto loc_evalrealheapsortstep1bb5in;
    }
   }
   if (nondet_bool()) {
    int Y_0 = nondet();
    if (2 + C >= 2 * Y_0 && 2 * Y_0 >= 1 + C && 0 >= Y_0 && 0 >= 2 + C) {
     goto loc_evalrealheapsortstep1bb5in;
    }
   }
  goto end;
 }
 loc_evalrealheapsortstep1bb5in:
 {
   if (nondet_bool()) {
    int B_ = 1 + B;
    if (1 >= 0) {
     B = B_;
     goto loc_evalrealheapsortstep1bb6in;
    }
   }
  goto end;
 }
 loc_evalrealheapsortstep1bb6in:
 {
   if (nondet_bool()) {
    int C_ = B;
    if (A >= 1 + B) {
     C = C_;
     goto loc_evalrealheapsortstep1bb3in;
    }
   }
   if (nondet_bool()) {
    if (B >= A) {
     goto loc_evalrealheapsortstep1returnin;
    }
   }
  goto end;
 }
 loc_evalrealheapsortstep1entryin:
 {
   if (nondet_bool()) {
    int B_ = 1;
    if (A >= 3) {
     B = B_;
     goto loc_evalrealheapsortstep1bb6in;
    }
   }
   if (nondet_bool()) {
    if (2 >= A) {
     goto loc_evalrealheapsortstep1returnin;
    }
   }
  goto end;
 }
 loc_evalrealheapsortstep1returnin:
 {
   if (nondet_bool()) {
    if (1 >= 0) {
     goto loc_evalrealheapsortstep1stop;
    }
   }
  goto end;
 }
 loc_evalrealheapsortstep1start:
 {
   if (nondet_bool()) {
    if (1 >= 0) {
     goto loc_evalrealheapsortstep1entryin;
    }
   }
  goto end;
 }
 loc_evalrealheapsortstep1stop:
 end: return 0;
}