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, int K1, int L1, int M1, int N1, int O1, int P1, int Q1, int R1, int S1, int T1, int U1, int V1, int W1, int X1, int Y1, int Z1, int A2, int B2, int C2, int D2, int E2, int F2, int G2, int H2, int I2, int J2, int K2, int L2, int M2, int N2, int O2, int P2, int Q2, int R2, int S2, int T2, int U2, int V2, int W2, int X2, int Y2, int Z2, int A3, int B3, int C3, int D3, int E3, int F3, int G3, int H3, int I3, int J3, int K3, int L3, int M3, int N3, int O3, int P3, int Q3, int R3, int S3, int T3, int U3, int V3, int W3) { goto loc_f0; loc_f0: { if (nondet_bool()) { int T3_ = nondet(); int S3_ = nondet(); int P3_ = nondet(); int O3_ = nondet(); int N3_ = nondet(); int M3_ = nondet(); int L3_ = nondet(); int K3_ = nondet(); int I3_ = nondet(); int H3_ = nondet(); int G3_ = nondet(); int F3_ = nondet(); int E3_ = nondet(); int D3_ = nondet(); int C3_ = nondet(); int U2_ = nondet(); int O1_ = nondet(); int L_ = nondet(); int V3_ = 7; int U3_ = 7; int R3_ = 0; int Q3_ = 0; int J3_ = 0; int B3_ = 0; int A3_ = 256; int Z2_ = 0; int Y2_ = 0; int X2_ = 0; int W2_ = 0; int V2_ = 0; int G2_ = 0; int F2_ = 9; int U1_ = 0; int K1_ = 0; int E1_ = 0; int U_ = 0; int B_ = 7; if (O1_ >= 1 && U2_ >= 1) { B = B_; L = L_; U = U_; E1 = E1_; K1 = K1_; O1 = O1_; U1 = U1_; F2 = F2_; G2 = G2_; U2 = U2_; V2 = V2_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; E3 = E3_; F3 = F3_; G3 = G3_; H3 = H3_; I3 = I3_; J3 = J3_; K3 = K3_; L3 = L3_; M3 = M3_; N3 = N3_; O3 = O3_; P3 = P3_; Q3 = Q3_; R3 = R3_; S3 = S3_; T3 = T3_; U3 = U3_; V3 = V3_; goto loc_f76; } } if (nondet_bool()) { int V3_ = nondet(); int U3_ = nondet(); int T3_ = nondet(); int S3_ = nondet(); int P3_ = nondet(); int O3_ = nondet(); int N3_ = nondet(); int M3_ = nondet(); int L3_ = nondet(); int K3_ = nondet(); int I3_ = nondet(); int H3_ = nondet(); int G3_ = nondet(); int F3_ = nondet(); int E3_ = nondet(); int D3_ = nondet(); int C3_ = nondet(); int U2_ = nondet(); int O1_ = nondet(); int L_ = nondet(); int B_ = nondet(); int W3_ = 1; int R3_ = 0; int Q3_ = 0; int J3_ = 0; int B3_ = 0; int A3_ = 256; int Z2_ = 0; int Y2_ = 0; int X2_ = 0; int W2_ = 0; int V2_ = 0; int G2_ = 0; int F2_ = 9; int U1_ = 0; int K1_ = 0; int E1_ = 0; int U_ = 0; if (O1_ >= 1 && U2_ >= 1 && 6 >= V3_) { B = B_; L = L_; U = U_; E1 = E1_; K1 = K1_; O1 = O1_; U1 = U1_; F2 = F2_; G2 = G2_; U2 = U2_; V2 = V2_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; E3 = E3_; F3 = F3_; G3 = G3_; H3 = H3_; I3 = I3_; J3 = J3_; K3 = K3_; L3 = L3_; M3 = M3_; N3 = N3_; O3 = O3_; P3 = P3_; Q3 = Q3_; R3 = R3_; S3 = S3_; T3 = T3_; U3 = U3_; V3 = V3_; W3 = W3_; goto loc_f76; } } if (nondet_bool()) { int V3_ = nondet(); int U3_ = nondet(); int T3_ = nondet(); int S3_ = nondet(); int P3_ = nondet(); int O3_ = nondet(); int N3_ = nondet(); int M3_ = nondet(); int L3_ = nondet(); int K3_ = nondet(); int I3_ = nondet(); int H3_ = nondet(); int G3_ = nondet(); int F3_ = nondet(); int E3_ = nondet(); int D3_ = nondet(); int C3_ = nondet(); int U2_ = nondet(); int O1_ = nondet(); int L_ = nondet(); int B_ = nondet(); int W3_ = 1; int R3_ = 0; int Q3_ = 0; int J3_ = 0; int B3_ = 0; int A3_ = 256; int Z2_ = 0; int Y2_ = 0; int X2_ = 0; int W2_ = 0; int V2_ = 0; int G2_ = 0; int F2_ = 9; int U1_ = 0; int K1_ = 0; int E1_ = 0; int U_ = 0; if (O1_ >= 1 && U2_ >= 1 && V3_ >= 8) { B = B_; L = L_; U = U_; E1 = E1_; K1 = K1_; O1 = O1_; U1 = U1_; F2 = F2_; G2 = G2_; U2 = U2_; V2 = V2_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; E3 = E3_; F3 = F3_; G3 = G3_; H3 = H3_; I3 = I3_; J3 = J3_; K3 = K3_; L3 = L3_; M3 = M3_; N3 = N3_; O3 = O3_; P3 = P3_; Q3 = Q3_; R3 = R3_; S3 = S3_; T3 = T3_; U3 = U3_; V3 = V3_; W3 = W3_; goto loc_f76; } } goto end; } loc_f105: { if (nondet_bool()) { int E2_ = nondet(); int D2_ = F1; int C2_ = 5; int B2_ = 1; int A2_ = 6; int Z1_ = 0; int Y1_ = -1 + Y1; if (Y1 >= 1) { Y1 = Y1_; Z1 = Z1_; A2 = A2_; B2 = B2_; C2 = C2_; D2 = D2_; E2 = E2_; goto loc_f105; } } if (nondet_bool()) { int F2_ = 8; if (0 >= Y1) { F2 = F2_; goto loc_f120; } } goto end; } loc_f120: { if (nondet_bool()) { int R1_ = nondet(); int Q1_ = nondet(); int T1_ = 0; int S1_ = 1; if (0 >= P1 && 0 >= U) { Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; goto loc_f137; } } if (nondet_bool()) { int R1_ = nondet(); int Q1_ = nondet(); int V1_ = U1; int U1_ = 1 + U1; int T1_ = 0; int S1_ = 1; if (P1 >= 1 && 0 >= U && P1 >= 1 + U1) { Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; goto loc_f137; } } if (nondet_bool()) { int R1_ = nondet(); int Q1_ = nondet(); int W1_ = 0; int V1_ = U1; int U1_ = 1 + U1; int T1_ = 0; int S1_ = 1; if (U1 >= P1 && 0 >= U && P1 >= 1) { Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; goto loc_f137; } } if (nondet_bool()) { int X1_ = 0; if (U >= 1) { X1 = X1_; goto loc_f219; } } goto end; } loc_f137: { if (nondet_bool()) { int H1_ = nondet(); int N1_ = 0; int M1_ = 0; int L1_ = 0; int K1_ = 0; int I1_ = -1; int A_ = 0; if (0 >= J1) { A = A_; H1 = H1_; I1 = I1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; goto loc_f155; } } if (nondet_bool()) { int H1_ = nondet(); int N1_ = 0; int M1_ = 0; int L1_ = 0; int K1_ = 0; int I1_ = -1; int A_ = 0; if (J1 >= 2) { A = A_; H1 = H1_; I1 = I1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; goto loc_f155; } } if (nondet_bool()) { int B_ = nondet(); int N1_ = 0; int M1_ = 0; int L1_ = 0; int K1_ = 0; int J1_ = 1; int F1_ = O1; int A1_ = 0; if (J1 == 1) { B = B_; A1 = A1_; F1 = F1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; goto loc_f178; } } goto end; } loc_f155: { if (nondet_bool()) { int B_ = 7; int A_ = 7; if (A == 7) { A = A_; B = B_; goto loc_f168; } } if (nondet_bool()) { int D_ = 0; int C_ = A; int B_ = A; if (6 >= A) { B = B_; C = C_; D = D_; goto loc_f160; } } if (nondet_bool()) { int D_ = 0; int C_ = A; int B_ = A; if (A >= 8) { B = B_; C = C_; D = D_; goto loc_f160; } } goto end; } loc_f160: { if (nondet_bool()) { int G_ = D; if (F >= 1 && D >= 1 && E >= 1) { G = G_; goto loc_f163; } } if (nondet_bool()) { int G1_ = 1; int G_ = D; if (0 >= D) { G = G_; G1 = G1_; goto loc_f168; } } if (nondet_bool()) { int H1_ = nondet(); int I1_ = -1; int G_ = D; int A_ = 0; if (0 >= F && D >= 1) { A = A_; G = G_; H1 = H1_; I1 = I1_; goto loc_f155; } } if (nondet_bool()) { int H1_ = nondet(); int I1_ = -1; int G_ = D; int A_ = 0; if (F >= 1 && D >= 1 && 0 >= E) { A = A_; G = G_; H1 = H1_; I1 = I1_; goto loc_f155; } } goto end; } loc_f163: { if (nondet_bool()) { if (1 >= 0) { goto loc_f163; } } goto end; } loc_f165: { if (nondet_bool()) { int H1_ = nondet(); int I1_ = -1; int A_ = 0; if (1 >= 0) { A = A_; H1 = H1_; I1 = I1_; goto loc_f155; } } goto end; } loc_f168: { if (nondet_bool()) { int B_ = nondet(); int F1_ = 1; int A1_ = 0; if (D1 >= 1 + E1) { B = B_; A1 = A1_; F1 = F1_; goto loc_f178; } } if (nondet_bool()) { int B_ = nondet(); int F1_ = 1; int E1_ = 0; int A1_ = 0; if (E1 >= D1) { B = B_; A1 = A1_; E1 = E1_; F1 = F1_; goto loc_f178; } } goto end; } loc_f178: { if (nondet_bool()) { int B1_ = A1; int Z_ = A1; if (3 >= B) { Z = Z_; B1 = B1_; goto loc_f186; } } if (nondet_bool()) { int B1_ = A1; int Z_ = A1; if (B >= 5) { Z = Z_; B1 = B1_; goto loc_f186; } } if (nondet_bool()) { int N_ = nondet(); int M_ = nondet(); int J_ = nondet(); int I_ = nondet(); int H_ = nondet(); int C1_ = 1; int B1_ = A1; int Z_ = A1; int O_ = 0; int K_ = L; int B_ = 4; if (B == 4) { B = B_; H = H_; I = I_; J = J_; K = K_; M = M_; N = N_; O = O_; Z = Z_; B1 = B1_; C1 = C1_; goto loc_f196; } } goto end; } loc_f186: { if (nondet_bool()) { int N_ = nondet(); int M_ = nondet(); int J_ = nondet(); int I_ = nondet(); int H_ = nondet(); int O_ = 0; int K_ = L; int B_ = 7; if (B == 7) { B = B_; H = H_; I = I_; J = J_; K = K_; M = M_; N = N_; O = O_; goto loc_f196; } } if (nondet_bool()) { if (6 >= B) { goto loc_f120; } } if (nondet_bool()) { if (B >= 8) { goto loc_f120; } } goto end; } loc_f196: { if (nondet_bool()) { int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int P_ = O; if (0 >= O) { P = P_; Q = Q_; R = R_; S = S_; goto loc_f209; } } if (nondet_bool()) { int X_ = nondet(); int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int Y_ = O; int W_ = O; int P_ = O; if (O >= 1) { P = P_; Q = Q_; R = R_; S = S_; W = W_; X = X_; Y = Y_; goto loc_f209; } } goto end; } loc_f209: { if (nondet_bool()) { int V_ = 7; int U_ = 1; int S_ = 7; if (S == 7) { S = S_; U = U_; V = V_; goto loc_f120; } } if (nondet_bool()) { int V_ = S; if (6 >= S) { V = V_; goto loc_f213; } } if (nondet_bool()) { int V_ = S; if (S >= 8) { V = V_; goto loc_f213; } } goto end; } loc_f213: { if (nondet_bool()) { int T_ = 0; if (T == 0) { T = T_; goto loc_f120; } } if (nondet_bool()) { int U_ = 1; if (0 >= 1 + T) { U = U_; goto loc_f120; } } if (nondet_bool()) { int U_ = 1; if (T >= 1) { U = U_; goto loc_f120; } } goto end; } loc_f219: { if (nondet_bool()) { if (1 >= 0) { goto loc_f219; } } goto end; } loc_f221: { if (nondet_bool()) { if (1 >= 0) { goto loc_f223; } } goto end; } loc_f76: { if (nondet_bool()) { int R2_ = nondet(); int N2_ = nondet(); int K2_ = nondet(); int J2_ = nondet(); int I2_ = nondet(); int Y1_ = nondet(); int J1_ = nondet(); int S2_ = 0; int Q2_ = J1; int P2_ = 0; int O2_ = 1; int M2_ = 0; int L2_ = L; int H2_ = G2; int F1_ = O1; if (0 >= G2 && Y1_ >= 1) { F1 = F1_; J1 = J1_; Y1 = Y1_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; O2 = O2_; P2 = P2_; Q2 = Q2_; R2 = R2_; S2 = S2_; goto loc_f105; } } if (nondet_bool()) { int R2_ = nondet(); int N2_ = nondet(); int K2_ = nondet(); int J2_ = nondet(); int I2_ = nondet(); int Y1_ = nondet(); int J1_ = nondet(); int T2_ = 1; int S2_ = 0; int Q2_ = J1; int P2_ = 0; int O2_ = 1; int M2_ = 0; int L2_ = L; int H2_ = G2; int F1_ = O1; if (G2 >= 1 && Y1_ >= 1) { F1 = F1_; J1 = J1_; Y1 = Y1_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; O2 = O2_; P2 = P2_; Q2 = Q2_; R2 = R2_; S2 = S2_; T2 = T2_; goto loc_f105; } } goto end; } loc_f223: end: return 0; }