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