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, int C1, int D1, int E1, int F1, int G1, int H1) { goto loc_f0; loc_f0: { if (nondet_bool()) { int X_ = nondet(); int W_ = nondet(); int V_ = 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_; V = V_; W = W_; X = X_; goto loc_f11; } } if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int G1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int B1_ = nondet(); int A1_ = nondet(); int Z_ = nondet(); int Y_ = nondet(); int W_ = nondet(); int V_ = nondet(); int O_ = nondet(); int M_ = nondet(); int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int E_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = nondet(); int A_ = nondet(); if (Y == 0 && 0 >= Y_0 && 0 >= K_ && 0 >= Y_1) { A = A_; B = B_; C = C_; D = D_; E = E_; J = J_; K = K_; L = L_; M = M_; O = O_; V = V_; W = W_; Y = Y_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f1; } } if (nondet_bool()) { int A1_ = nondet(); int Z_ = nondet(); int W_ = nondet(); int V_ = nondet(); int N_ = nondet(); int L_ = nondet(); int E_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = nondet(); int A_ = nondet(); int O_ = J; int M_ = J; int K_ = 1; if (0 >= 1 + J) { A = A_; B = B_; C = C_; D = D_; E = E_; K = K_; L = L_; M = M_; N = N_; O = O_; V = V_; W = W_; Z = Z_; A1 = A1_; goto loc_f5; } } if (nondet_bool()) { int A1_ = nondet(); int Z_ = nondet(); int W_ = nondet(); int V_ = nondet(); int N_ = nondet(); int L_ = nondet(); int E_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = nondet(); int A_ = nondet(); int O_ = J; int M_ = J; int K_ = 1; if (J >= 1) { A = A_; B = B_; C = C_; D = D_; E = E_; K = K_; L = L_; M = M_; N = N_; O = O_; V = V_; W = W_; Z = Z_; A1 = A1_; goto loc_f5; } } goto end; } loc_f11: { if (nondet_bool()) { int F_ = nondet(); int D_ = nondet(); int H_ = I; 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_; H = H_; goto loc_f11; } } if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int A1_ = nondet(); int Z_ = nondet(); int W_ = nondet(); int N_ = nondet(); int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = nondet(); int A_ = nondet(); int O_ = J; int M_ = J; if (H1 >= 0 && 0 >= 1 + J && K_ >= 2 && B >= 0 && B >= A && H1 >= Y_0 && Y_0 >= 2 && H1 >= Y_1 && Y_1 >= 2) { A = A_; B = B_; C = C_; D = D_; E = E_; K = K_; L = L_; M = M_; N = N_; O = O_; W = W_; Z = Z_; A1 = A1_; goto loc_f2; } } if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int A1_ = nondet(); int Z_ = nondet(); int W_ = nondet(); int N_ = nondet(); int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); int C_ = nondet(); int B_ = nondet(); int A_ = nondet(); int O_ = J; int M_ = J; if (H1 >= 0 && J >= 1 && K_ >= 2 && B >= 0 && B >= A && H1 >= Y_0 && Y_0 >= 2 && H1 >= Y_1 && Y_1 >= 2) { A = A_; B = B_; C = C_; D = D_; E = E_; K = K_; L = L_; M = M_; N = N_; O = O_; W = W_; Z = Z_; A1 = A1_; goto loc_f2; } } goto end; } loc_f2: { if (nondet_bool()) { int N_ = nondet(); int L_ = nondet(); int K_ = nondet(); int R_ = I; int P_ = Q; int O_ = J; int M_ = J; if (K_ >= 2 && 0 >= 1 + J) { K = K_; L = L_; M = M_; N = N_; O = O_; P = P_; R = R_; goto loc_f2; } } if (nondet_bool()) { int N_ = nondet(); int L_ = nondet(); int K_ = nondet(); int R_ = I; int P_ = Q; int O_ = J; int M_ = J; if (K_ >= 2 && J >= 1) { K = K_; L = L_; M = M_; N = N_; O = O_; P = P_; R = R_; goto loc_f2; } } goto end; } loc_f5: { if (nondet_bool()) { int N_ = nondet(); int L_ = nondet(); int T_ = U; int S_ = I; int O_ = J; int M_ = J; int K_ = 1; if (0 >= 1 + J) { K = K_; L = L_; M = M_; N = N_; O = O_; S = S_; T = T_; goto loc_f5; } } if (nondet_bool()) { int N_ = nondet(); int L_ = nondet(); int T_ = U; int S_ = I; int O_ = J; int M_ = J; int K_ = 1; if (J >= 1) { K = K_; L = L_; M = M_; N = N_; O = O_; S = S_; T = T_; goto loc_f5; } } goto end; } loc_f1: end: return 0; }