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, int S, int T, int U, int V, int W, int X, int Y, int Z, int A1, int B1) { goto loc_f8; loc_f1: { if (nondet_bool()) { int N_ = nondet(); int L_ = nondet(); int O_ = J; int M_ = L; int K_ = L; int J_ = 1 + J; if (J >= 0 && I >= 1 + J) { J = J_; K = K_; L = L_; M = M_; N = N_; O = O_; goto loc_f1; } } if (nondet_bool()) { int Y_0 = nondet(); int B1_ = nondet(); int Z_ = nondet(); int Y_ = nondet(); int Q_ = nondet(); int M_ = nondet(); int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int I_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = K; if (0 >= 1 + D_ && 0 >= 1 + K && C_ >= 2 && B1_ >= C_ && J_ >= 0 && J_ >= Y_0 && Y_0 >= 2 && J >= 0 && J >= I) { B = B_; C = C_; D = D_; I = I_; J = J_; K = K_; L = L_; M = M_; Q = Q_; Y = Y_; Z = Z_; B1 = B1_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int B1_ = nondet(); int Z_ = nondet(); int Y_ = nondet(); int Q_ = nondet(); int M_ = nondet(); int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int I_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = K; if (D_ >= 1 && 0 >= 1 + K && C_ >= 2 && B1_ >= C_ && J_ >= 0 && J_ >= Y_0 && Y_0 >= 2 && J >= 0 && J >= I) { B = B_; C = C_; D = D_; I = I_; J = J_; K = K_; L = L_; M = M_; Q = Q_; Y = Y_; Z = Z_; B1 = B1_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int B1_ = nondet(); int Z_ = nondet(); int Y_ = nondet(); int Q_ = nondet(); int M_ = nondet(); int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int I_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = K; if (0 >= 1 + D_ && K >= 1 && C_ >= 2 && B1_ >= C_ && J_ >= 0 && J_ >= Y_0 && Y_0 >= 2 && J >= 0 && J >= I) { B = B_; C = C_; D = D_; I = I_; J = J_; K = K_; L = L_; M = M_; Q = Q_; Y = Y_; Z = Z_; B1 = B1_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int B1_ = nondet(); int Z_ = nondet(); int Y_ = nondet(); int Q_ = nondet(); int M_ = nondet(); int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int I_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = K; if (D_ >= 1 && K >= 1 && C_ >= 2 && B1_ >= C_ && J_ >= 0 && J_ >= Y_0 && Y_0 >= 2 && J >= 0 && J >= I) { B = B_; C = C_; D = D_; I = I_; J = J_; K = K_; L = L_; M = M_; Q = Q_; Y = Y_; Z = Z_; B1 = B1_; goto loc_f12; } } goto end; } loc_f12: { if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int C_ = nondet(); int H_ = A; int F_ = G; int E_ = B; if (0 >= 1 + B && 0 >= 1 + D_ && 0 >= 1 + Y_0 && C_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int C_ = nondet(); int H_ = A; int F_ = G; int E_ = B; if (B >= 1 && 0 >= 1 + D_ && 0 >= 1 + Y_0 && C_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int C_ = nondet(); int H_ = A; int F_ = G; int E_ = B; if (0 >= 1 + B && D_ >= 1 && 0 >= 1 + Y_0 && C_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int C_ = nondet(); int H_ = A; int F_ = G; int E_ = B; if (B >= 1 && D_ >= 1 && 0 >= 1 + Y_0 && C_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int C_ = nondet(); int H_ = A; int F_ = G; int E_ = B; if (0 >= 1 + B && 0 >= 1 + D_ && Y_0 >= 1 && C_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int C_ = nondet(); int H_ = A; int F_ = G; int E_ = B; if (B >= 1 && 0 >= 1 + D_ && Y_0 >= 1 && C_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int C_ = nondet(); int H_ = A; int F_ = G; int E_ = B; if (0 >= 1 + B && D_ >= 1 && Y_0 >= 1 && C_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; goto loc_f12; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int C_ = nondet(); int H_ = A; int F_ = G; int E_ = B; if (B >= 1 && D_ >= 1 && Y_0 >= 1 && C_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; goto loc_f12; } } goto end; } loc_f8: { if (nondet_bool()) { int R_ = nondet(); int Q_ = nondet(); int P_ = nondet(); int M_ = nondet(); int L_ = nondet(); int K_ = nondet(); int I_ = nondet(); int C_ = nondet(); int S_ = 2; int J_ = 2; if (I_ >= 2) { C = C_; I = I_; J = J_; K = K_; L = L_; M = M_; P = P_; Q = Q_; R = R_; S = S_; goto loc_f1; } } if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int Y_2 = nondet(); int A1_ = nondet(); int Z_ = nondet(); int Y_ = nondet(); int X_ = nondet(); int W_ = nondet(); int V_ = nondet(); int U_ = nondet(); int T_ = nondet(); int Q_ = nondet(); int P_ = nondet(); int M_ = nondet(); int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int I_ = nondet(); int C_ = nondet(); int D_ = 0; int B_ = 0; if (0 >= Y_0 && 0 >= C_ && 0 >= Y_1 && 0 >= Y_2) { B = B_; C = C_; D = D_; I = I_; J = J_; K = K_; L = L_; M = M_; P = P_; Q = Q_; T = T_; U = U_; V = V_; W = W_; X = X_; Y = Y_; Z = Z_; A1 = A1_; goto loc_f9; } } goto end; } loc_f9: end: return 0; }