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