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