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, int X3, int Y3, int Z3, int A4, int B4, int C4, int D4, int E4, int F4, int G4, int H4, int I4, int J4, int K4, int L4, int M4, int N4, int O4, int P4, int Q4, int R4, int S4, int T4, int U4, int V4, int W4, int X4, int Y4, int Z4, int A5, int B5, int C5, int D5, int E5, int F5, int G5, int H5, int I5, int J5, int K5, int L5, int M5, int N5, int O5, int P5, int Q5, int R5, int S5, int T5, int U5, int V5, int W5, int X5, int Y5, int Z5, int A6) { goto loc_f14; loc_f1: { if (nondet_bool()) { int G4_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int V_ = nondet(); int P_ = nondet(); int W_ = -1 + W; int G_ = Z3; int E_ = X3; int D_ = W3; if (E1_ >= 1 + F4 && W3 >= 1 + X3 && I1_ >= 1 + E4 && V_ >= 1 + Y3 && C4 >= 1 + D4 && A4 >= 1 + B4 && Z3 >= 1 && W >= 1) { D = D_; E = E_; G = G_; P = P_; V = V_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; G4 = G4_; goto loc_f34; } } goto end; } loc_f10: { if (nondet_bool()) { int V_ = nondet(); int P_ = nondet(); int W_ = -1 + W; int G_ = V3; int E_ = X3; int D_ = W3; if (V_ >= 1 + Y3 && W3 >= 1 + X3 && V3 >= 1 && W >= 1) { D = D_; E = E_; G = G_; P = P_; V = V_; W = W_; goto loc_f34; } } goto end; } loc_f14: { if (nondet_bool()) { int T5_ = nondet(); int S5_ = nondet(); int R5_ = nondet(); int Q5_ = nondet(); int P5_ = nondet(); int O5_ = nondet(); int N5_ = nondet(); int M5_ = nondet(); int L5_ = nondet(); int K5_ = nondet(); int W4_ = nondet(); int V_ = nondet(); int P_ = nondet(); int G_ = nondet(); int W_ = -1 + T5_; int E_ = H5; int D_ = G5; if (I5 >= 1 + J5 && G5 >= 1 + H5 && V_ >= 1 + F5 && M5_ >= 1 + E5 && 0 >= K5_ && T5_ >= 1 && 0 >= N5_) { D = D_; E = E_; G = G_; P = P_; V = V_; W = W_; W4 = W4_; K5 = K5_; L5 = L5_; M5 = M5_; N5 = N5_; O5 = O5_; P5 = P5_; Q5 = Q5_; R5 = R5_; S5 = S5_; T5 = T5_; goto loc_f36; } } if (nondet_bool()) { int T5_ = nondet(); int S5_ = nondet(); int R5_ = nondet(); int Q5_ = nondet(); int P5_ = nondet(); int O5_ = nondet(); int N5_ = nondet(); int M5_ = nondet(); int L5_ = nondet(); int W4_ = nondet(); int V_ = nondet(); int P_ = nondet(); int W_ = -1 + T5_; int G_ = U5; int E_ = Y5; int D_ = X5; if (Z5 >= 1 + A6 && X5 >= 1 + Y5 && V_ >= 1 + W5 && M5_ >= 1 + V5 && U5 >= 1 && T5_ >= 1 && N5_ >= 1) { D = D_; E = E_; G = G_; P = P_; V = V_; W = W_; W4 = W4_; L5 = L5_; M5 = M5_; N5 = N5_; O5 = O5_; P5 = P5_; Q5 = Q5_; R5 = R5_; S5 = S5_; T5 = T5_; goto loc_f35; } } goto end; } loc_f16: { if (nondet_bool()) { int L1_ = nondet(); int K1_ = nondet(); int J1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int G1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int W_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G_ = W; if (I1_ >= 1 + C1 && E1_ >= 1 + B1 && Z >= 1 + A1 && X >= 1 + Y && 0 >= W_ && 0 >= W) { D = D_; E = E_; G = G_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; goto loc_f0; } } if (nondet_bool()) { int V4_ = nondet(); int U4_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int V_ = nondet(); int P_ = nondet(); int J_ = nondet(); int U1_ = K1; int W_ = -1 + W; int I_ = -W + V4_; int H_ = -W + V4_; int G_ = Z3; int F_ = K1; int E_ = X3; int D_ = W3; if (W3 >= 1 + X3 && S4 >= 1 + T4 && E1_ >= 1 + R4 && I1_ >= 1 + Q4 && V_ >= 1 + Y3 && O4 >= 1 + P4 && Z3 >= 1 && W >= 1) { D = D_; E = E_; F = F_; G = G_; H = H_; I = I_; J = J_; P = P_; V = V_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; U1 = U1_; U4 = U4_; V4 = V4_; goto loc_f34; } } goto end; } loc_f17: { if (nondet_bool()) { int U1_ = nondet(); int T1_ = nondet(); int S1_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int W_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G_ = W; if (I1_ >= 1 + R1 && E1_ >= 1 + Q1 && O1 >= 1 + P1 && M1 >= 1 + N1 && 0 >= W_ && 0 >= W) { D = D_; E = E_; G = G_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; L1 = L1_; S1 = S1_; T1 = T1_; U1 = U1_; goto loc_f0; } } if (nondet_bool()) { int U4_ = nondet(); int U1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int V_ = nondet(); int P_ = nondet(); int W_ = -1 + W; int G_ = Z3; int E_ = X3; int D_ = W3; if (W3 >= 1 + X3 && S4 >= 1 + T4 && E1_ >= 1 + R4 && I1_ >= 1 + Q4 && V_ >= 1 + Y3 && O4 >= 1 + P4 && Z3 >= 1 && W >= 1) { D = D_; E = E_; G = G_; P = P_; V = V_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; U1 = U1_; U4 = U4_; goto loc_f34; } } goto end; } loc_f19: { if (nondet_bool()) { int R_ = nondet(); int Q_ = nondet(); int P_ = Q; int E_ = O; int D_ = N; if (N >= 1 + O && R_ >= 1 + M) { D = D_; E = E_; P = P_; Q = Q_; R = R_; goto loc_f34; } } goto end; } loc_f2: { if (nondet_bool()) { int N4_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int V_ = nondet(); int P_ = nondet(); int W_ = -1 + W; int G_ = Z3; int E_ = X3; int D_ = W3; if (E1_ >= 1 + M4 && W3 >= 1 + X3 && I1_ >= 1 + L4 && V_ >= 1 + Y3 && J4 >= 1 + K4 && H4 >= 1 + I4 && Z3 >= 1 && W >= 1) { D = D_; E = E_; G = G_; P = P_; V = V_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; N4 = N4_; goto loc_f34; } } goto end; } loc_f33: { if (nondet_bool()) { int R_ = nondet(); int Q_ = nondet(); int P_ = Q; int G_ = V1; int E_ = Z1; int D_ = Y1; if (Y1 >= 1 + Z1 && 0 >= X1 && R_ >= 1 + W1 && V1 >= 1) { D = D_; E = E_; G = G_; P = P_; Q = Q_; R = R_; goto loc_f34; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int I_ = nondet(); int G_ = C2; int E_ = F2; int D_ = E2; if (E2 >= 1 + F2 && L_ >= 1 + D2 && X1 >= 1 && C2 >= 1) { D = D_; E = E_; G = G_; I = I_; J = J_; K = K_; L = L_; goto loc_f17; } } goto end; } loc_f34: { if (nondet_bool()) { int R_ = nondet(); int Q_ = nondet(); int P_ = Q; int G_ = A2; int E_ = Z1; int D_ = Y1; if (Y1 >= 1 + Z1 && 0 >= B2 && R_ >= 1 + W1 && A2 >= 1) { D = D_; E = E_; G = G_; P = P_; Q = Q_; R = R_; goto loc_f34; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int I_ = nondet(); int G_ = G2; int E_ = F2; int D_ = E2; if (E2 >= 1 + F2 && L_ >= 1 + D2 && B2 >= 1 && G2 >= 1) { D = D_; E = E_; G = G_; I = I_; J = J_; K = K_; L = L_; goto loc_f17; } } goto end; } loc_f35: { if (nondet_bool()) { int R_ = nondet(); int Q_ = nondet(); int P_ = Q; int G_ = H2; int E_ = L2; int D_ = K2; if (K2 >= 1 + L2 && 0 >= J2 && R_ >= 1 + I2 && H2 >= 1) { D = D_; E = E_; G = G_; P = P_; Q = Q_; R = R_; goto loc_f35; } } if (nondet_bool()) { int A3_ = nondet(); int Z2_ = nondet(); int Y2_ = nondet(); int X2_ = nondet(); int W2_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int W_ = nondet(); int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G_ = W; if (I1_ >= 1 + V2 && E1_ >= 1 + U2 && L_ >= 1 + T2 && R2 >= 1 + S2 && P2 >= 1 + Q2 && N2 >= 1 + O2 && J2 >= 1 && M2 >= 1 && 0 >= W_ && 0 >= W) { D = D_; E = E_; G = G_; K = K_; L = L_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; L1 = L1_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; goto loc_f0; } } if (nondet_bool()) { int V4_ = nondet(); int U4_ = nondet(); int A3_ = nondet(); int Z2_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int V_ = nondet(); int P_ = nondet(); int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int U1_ = W4; int W_ = -1 + W; int I_ = -W + V4_; int H_ = -W + V4_; int G_ = Z3; int F_ = W4; int E_ = X3; int D_ = W3; if (W3 >= 1 + X3 && S4 >= 1 + T4 && E1_ >= 1 + R4 && I1_ >= 1 + Q4 && L_ >= 1 + T2 && V_ >= 1 + Y3 && O4 >= 1 + P4 && N2 >= 1 + O2 && J2 >= 1 && M2 >= 1 && Z3 >= 1 && W >= 1) { D = D_; E = E_; F = F_; G = G_; H = H_; I = I_; J = J_; K = K_; L = L_; P = P_; V = V_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; U1 = U1_; Z2 = Z2_; A3 = A3_; U4 = U4_; V4 = V4_; goto loc_f34; } } goto end; } loc_f36: { if (nondet_bool()) { int F3_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int G_ = nondet(); int P_ = Q; int E_ = E3; int D_ = D3; if (D3 >= 1 + E3 && 0 >= C3 && R_ >= 1 + B3 && 0 >= F3_) { D = D_; E = E_; G = G_; P = P_; Q = Q_; R = R_; F3 = F3_; goto loc_f36; } } if (nondet_bool()) { int U3_ = nondet(); int T3_ = nondet(); int S3_ = nondet(); int R3_ = nondet(); int Q3_ = nondet(); int P3_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int W_ = nondet(); int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G_ = W; if (I1_ >= 1 + O3 && E1_ >= 1 + N3 && L_ >= 1 + M3 && K3 >= 1 + L3 && I3 >= 1 + J3 && G3 >= 1 + H3 && C3 >= 1 && 0 >= W_ && 0 >= U3_ && 0 >= W) { D = D_; E = E_; G = G_; K = K_; L = L_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; L1 = L1_; P3 = P3_; Q3 = Q3_; R3 = R3_; S3 = S3_; T3 = T3_; U3 = U3_; goto loc_f0; } } if (nondet_bool()) { int D5_ = nondet(); int U3_ = nondet(); int T3_ = nondet(); int S3_ = nondet(); int R3_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int V_ = nondet(); int P_ = nondet(); int L_ = nondet(); int K_ = nondet(); int W_ = -1 + W; int G_ = Z3; int E_ = X3; int D_ = W3; if (B5 >= 1 + C5 && W3 >= 1 + X3 && E1_ >= 1 + A5 && I1_ >= 1 + Z4 && L_ >= 1 + M3 && V_ >= 1 + Y3 && X4 >= 1 + Y4 && G3 >= 1 + H3 && C3 >= 1 && Z3 >= 1 && 0 >= U3_ && W >= 1) { D = D_; E = E_; G = G_; K = K_; L = L_; P = P_; V = V_; W = W_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; R3 = R3_; S3 = S3_; T3 = T3_; U3 = U3_; D5 = D5_; goto loc_f34; } } goto end; } loc_f38: { if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int J_ = nondet(); int H_ = nondet(); int I_ = -G + J_; int F_ = -G + J_; int E_ = C; int D_ = B; if (B >= 1 + C && L_ >= 1 + A) { D = D_; E = E_; F = F_; H = H_; I = I_; J = J_; K = K_; L = L_; goto loc_f17; } } goto end; } loc_f50: { if (nondet_bool()) { int V_ = nondet(); int P_ = nondet(); int E_ = U; int D_ = T; if (T >= 1 + U && V_ >= 1 + S) { D = D_; E = E_; P = P_; V = V_; goto loc_f34; } } goto end; } loc_f0: end: return 0; }