int nondet() { int a; return a; } _Bool nondet_bool() { _Bool a; return a; } int foo (int A, int B, int C, int D, int E, int F, int G, int H, int I, int J, int K, int L, int M, int N, int O, int P, int Q, int R) { goto loc_f2; loc_f13: { if (nondet_bool()) { int E_ = nondet(); int D_ = nondet(); int F_ = 1; int C_ = 1 + B; if (A >= B) { C = C_; D = D_; E = E_; F = F_; goto loc_f20; } } if (nondet_bool()) { if (B >= 1 + A) { goto loc_f1; } } goto end; } loc_f2: { if (nondet_bool()) { int A_ = 1; if (A == 1) { A = A_; goto loc_f1; } } if (nondet_bool()) { int B_ = 1; if (0 >= A) { B = B_; goto loc_f13; } } if (nondet_bool()) { int B_ = 1; if (A >= 2) { B = B_; goto loc_f13; } } goto end; } loc_f20: { if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int Y_2 = nondet(); int Y_3 = nondet(); int F_ = 1 + F; int E_ = E + Y_2 * Y_3; int D_ = D + Y_0 * Y_1; if (B >= F) { D = D_; E = E_; F = F_; goto loc_f20; } } if (nondet_bool()) { int F_ = 1; if (F >= 1 + B && 0 >= 1 + E) { F = F_; goto loc_f31; } } if (nondet_bool()) { int F_ = 1; if (F >= 1 + B && E >= 1) { F = F_; goto loc_f31; } } if (nondet_bool()) { int F_ = 1; int E_ = 0; if (E == 0 && F >= 1 + B) { E = E_; F = F_; goto loc_f31; } } goto end; } loc_f31: { if (nondet_bool()) { int F_ = 1 + F; if (B >= F) { F = F_; goto loc_f31; } } if (nondet_bool()) { int C_ = A; if (A == C && F >= 1 + B) { C = C_; goto loc_f1; } } if (nondet_bool()) { int I_ = nondet(); int H_ = nondet(); int G_ = nondet(); int F_ = 1; if (F >= 1 + B && A >= 1 + C) { F = F_; G = G_; H = H_; I = I_; goto loc_f45; } } if (nondet_bool()) { int I_ = nondet(); int H_ = nondet(); int G_ = nondet(); int F_ = 1; if (F >= 1 + B && C >= 1 + A) { F = F_; G = G_; H = H_; I = I_; goto loc_f45; } } goto end; } loc_f45: { if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int Y_2 = nondet(); int Y_3 = nondet(); int Y_4 = nondet(); int Y_5 = nondet(); int I_ = I + Y_4 * Y_5; int H_ = H + Y_2 * Y_3; int G_ = G + Y_0 * Y_1; int F_ = 1 + F; if (B >= F) { F = F_; G = G_; H = H_; I = I_; goto loc_f45; } } if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int R_ = nondet(); int Q_ = nondet(); int J_ = nondet(); int K_ = B; int F_ = 1; if (F >= 1 + B && J_ >= Y_0 && 3 * Y_0 >= 2 + B && 1 + B >= 2 * Y_0 && Y_1 >= J_ && 3 * Y_1 >= 2 + B && 1 + B >= 2 * Y_1) { F = F_; J = J_; K = K_; Q = Q_; R = R_; goto loc_f60; } } goto end; } loc_f60: { if (nondet_bool()) { int O_ = nondet(); int N_ = nondet(); int M_ = nondet(); int L_ = nondet(); int P_ = K; int K_ = -1 + K; int F_ = 1 + F; if (J >= F) { F = F_; K = K_; L = L_; M = M_; N = N_; O = O_; P = P_; goto loc_f60; } } if (nondet_bool()) { int B_ = 1 + B; if (F >= 1 + J) { B = B_; goto loc_f13; } } goto end; } loc_f1: end: return 0; }