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, int I1, int J1) { goto loc_f6; loc_f11: { if (nondet_bool()) { int Y_0 = nondet(); int G_ = nondet(); int F_ = nondet(); int H_ = B; int E_ = 2 + C; if (E == 1 + C && D >= 0 && C >= 1 && Y_0 >= 1 && B >= 0 && B >= A && A >= 2) { E = E_; F = F_; G = G_; H = H_; goto loc_f15; } } if (nondet_bool()) { int I_ = nondet(); int G_ = nondet(); int J_ = -1; int F_ = 0; int D_ = -1 + I_; if (F == 0 && E >= 1 && I_ >= 1 && B >= 0 && I >= A && B >= A && A >= 2) { D = D_; F = F_; G = G_; I = I_; J = J_; goto loc_f14; } } if (nondet_bool()) { int D1_ = nondet(); if (A >= 2 && 0 >= E && B >= 0 && B >= A) { D1 = D1_; goto loc_f7; } } goto end; } loc_f13: { if (nondet_bool()) { int Y_0 = nondet(); int G_ = nondet(); int F_ = nondet(); int L_ = M; int E_ = 2 + K; int A_ = 1; if (A == 1 && E == 1 + K && K >= 1 && Y_0 >= 1) { A = A_; E = E_; F = F_; G = G_; L = L_; goto loc_f13; } } if (nondet_bool()) { int D1_ = nondet(); int G_ = nondet(); int Q_ = 0; int F_ = 0; int A_ = 1; if (F == 0 && A == 1 && Q == 0 && E >= 1) { A = A_; F = F_; G = G_; Q = Q_; D1 = D1_; goto loc_f7; } } if (nondet_bool()) { int D1_ = nondet(); int A_ = 1; if (A == 1 && 0 >= E) { A = A_; D1 = D1_; goto loc_f7; } } goto end; } loc_f14: { if (nondet_bool()) { int P_ = nondet(); int N_ = nondet(); int G_ = nondet(); int F_ = nondet(); int D_ = nondet(); int O_ = 1 + N; int E_ = 2 + N; if (F == 0 && D >= 0 && P_ >= 0 && N >= 1 && E >= 1 && A >= 2) { D = D_; E = E_; F = F_; G = G_; N = N_; O = O_; P = P_; goto loc_f15; } } if (nondet_bool()) { int S_ = nondet(); int G_ = nondet(); int D_ = nondet(); int R_ = Q; int F_ = 0; if (Q == R && F == 0 && D >= 0 && S_ >= 0 && E >= 1 && A >= 2) { D = D_; F = F_; G = G_; R = R_; S = S_; goto loc_f14; } } if (nondet_bool()) { int D1_ = nondet(); int Q_ = 0; int F_ = 0; int D_ = 0; if (D == 0 && F == 0 && Q == 0 && A >= 2 && E >= 1) { D = D_; F = F_; Q = Q_; D1 = D1_; goto loc_f7; } } goto end; } loc_f15: { if (nondet_bool()) { int Y_0 = nondet(); int U_ = nondet(); int G_ = nondet(); int F_ = nondet(); int D_ = nondet(); int E_ = 2 + T; if (E == 1 + T && D >= 0 && U_ >= 0 && Y_0 >= 1 && T >= 1 && A >= 2) { D = D_; E = E_; F = F_; G = G_; U = U_; goto loc_f15; } } if (nondet_bool()) { int W_ = nondet(); int G_ = nondet(); int D_ = nondet(); int V_ = Q; int F_ = 0; if (Q == V && F == 0 && D >= 0 && W_ >= 0 && E >= 1 && A >= 2) { D = D_; F = F_; G = G_; V = V_; W = W_; goto loc_f14; } } if (nondet_bool()) { int D1_ = nondet(); if (A >= 2 && 0 >= E && D >= 0) { D1 = D1_; goto loc_f7; } } goto end; } loc_f17: { if (nondet_bool()) { int Y_0 = nondet(); int C1_ = nondet(); int B1_ = C1; int A1_ = Z; int Z_ = C1; int Y_ = -1 + B; int X_ = A; int B_ = 1 + B; if (B1 == A1 && Z == A1 && A == X && 1 + Y == B && X >= 2 && Y_0 >= 0 && X >= 1 + Y_0 && X >= B) { B = B_; X = X_; Y = Y_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; goto loc_f17; } } if (nondet_bool()) { int G1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int B1_ = nondet(); int A1_ = nondet(); int Z_ = nondet(); int X_ = nondet(); int G_ = nondet(); int F_ = nondet(); int B_ = nondet(); int H1_ = B; int F1_ = 101; int Q_ = Z; int E_ = 102; if (B1 == A1 && Z == A1 && A == X && E == 100 && X >= 2 && G1_ >= 0 && G1_ >= X && B >= 0 && B >= X && D >= 0) { B = B_; E = E_; F = F_; G = G_; Q = Q_; X = X_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; goto loc_f15; } } if (nondet_bool()) { int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int B1_ = nondet(); int A1_ = nondet(); int Z_ = nondet(); int X_ = nondet(); int G_ = nondet(); int B_ = nondet(); int H1_ = B; int Q_ = J1; int F_ = 0; int E_ = 100; if (B1 == A1 && Z == A1 && J1 == A1 && A == X && F == 0 && E == 100 && I1 >= X && X >= 2 && B_ >= 0 && B_ >= X && B >= 0 && B >= X && D >= 0) { B = B_; E = E_; F = F_; G = G_; Q = Q_; X = X_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; H1 = H1_; goto loc_f14; } } goto end; } loc_f6: { if (nondet_bool()) { int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int B1_ = nondet(); int A1_ = nondet(); int Z_ = nondet(); int X_ = nondet(); int G_ = nondet(); int B_ = nondet(); int A_ = nondet(); int Q_ = 0; int E_ = 100; if (Z == 0 && A == X && B == 0 && E == 100 && Q == 0 && 0 >= A_) { A = A_; B = B_; E = E_; G = G_; Q = Q_; X = X_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; goto loc_f7; } } goto end; } loc_f7: end: return 0; }