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) { goto loc_f19; loc_f1: { if (nondet_bool()) { int E1_ = nondet(); int F1_ = E1; int D1_ = E1; int B_ = 1 + B; if (C1 >= 1 + B && B >= 0) { B = B_; D1 = D1_; E1 = E1_; F1 = F1_; goto loc_f1; } } if (nondet_bool()) { int Y_0 = nondet(); int B2_ = nondet(); int A2_ = nondet(); int Z1_ = nondet(); int Y1_ = nondet(); int P1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int Z_ = nondet(); int C_ = nondet(); int B_ = nondet(); int C2_ = H; int R1_ = D1; int Q1_ = D1; int D_ = 0; if (D == 0 && B >= 0 && H >= 0 && H >= A && A >= 2 && B >= C1 && Z1_ >= A && Y_0 >= A) { B = B_; C = C_; D = D_; Z = Z_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; P1 = P1_; Q1 = Q1_; R1 = R1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; B2 = B2_; C2 = C2_; goto loc_f18; } } goto end; } loc_f10: { if (nondet_bool()) { int G1_ = nondet(); int K1_ = -1; int J1_ = -1 + G1_; int H1_ = I1; if (G1 >= 0) { G1 = G1_; H1 = H1_; J1 = J1_; K1 = K1_; goto loc_f11; } } if (nondet_bool()) { int P1_ = nondet(); int O1_ = nondet(); int N1_ = nondet(); int M1_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); if (L1 == I1 && G1 >= 0) { H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f20; } } goto end; } loc_f11: { if (nondet_bool()) { int S1_ = -1 + J1; int Q1_ = 0; int O1_ = R1; int N1_ = 0; int M1_ = R1; int L1_ = 0; int J1_ = -1 + J1; int H1_ = I1; if (L1 == 0 && M1 == O1 && N1 == 0 && R1 == O1 && Q1 == 0 && C >= 1 && J1 >= 0 && A >= 2) { H1 = H1_; J1 = J1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; Q1 = Q1_; S1 = S1_; goto loc_f11; } } if (nondet_bool()) { int P1_ = nondet(); int O1_ = nondet(); int N1_ = nondet(); int M1_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int A_ = nondet(); if (L1 == I1 && J1 >= 0) { A = A_; H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f20; } } goto end; } loc_f12: { if (nondet_bool()) { int T1_ = nondet(); int V1_ = -1; int U1_ = -1 + T1_; int H1_ = I1; if (T1 >= 0) { H1 = H1_; T1 = T1_; U1 = U1_; V1 = V1_; goto loc_f13; } } if (nondet_bool()) { int P1_ = nondet(); int O1_ = nondet(); int N1_ = nondet(); int M1_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); if (L1 == I1 && T1 >= 0) { H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f20; } } goto end; } loc_f13: { if (nondet_bool()) { int W1_ = -1 + U1; int U1_ = -1 + U1; int Q1_ = 0; int O1_ = R1; int N1_ = 0; int M1_ = R1; int L1_ = 0; int H1_ = I1; if (L1 == 0 && M1 == O1 && N1 == 0 && R1 == O1 && Q1 == 0 && 0 >= C && U1 >= 0 && A >= 2) { H1 = H1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; Q1 = Q1_; U1 = U1_; W1 = W1_; goto loc_f13; } } if (nondet_bool()) { int P1_ = nondet(); int O1_ = nondet(); int N1_ = nondet(); int M1_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); if (L1 == I1 && U1 >= 0) { H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f20; } } goto end; } loc_f14: { if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int M_ = nondet(); int L_ = nondet(); int K_ = nondet(); int I_ = nondet(); int J_ = 1 + H; int G_ = H; int F_ = -1 + Y_0; int E_ = -1; int D_ = 1; int C_ = -1 + Y_0; if (D == 1 && Y_0 >= 1 && C >= 1 && B >= 0 && Y_1 >= A && A >= 2) { C = C_; D = D_; E = E_; F = F_; G = G_; I = I_; J = J_; K = K_; L = L_; M = M_; goto loc_f18; } } if (nondet_bool()) { int Z1_ = nondet(); int Y1_ = nondet(); int Z_ = nondet(); int C_ = nondet(); int B_ = nondet(); int X1_ = B; int R1_ = Q1; int H_ = B; int D_ = 0; if (D == 0 && B == H && Q1 == R1 && H >= 0 && 0 >= C && H >= A && A >= 2 && Z1_ >= A) { B = B_; C = C_; D = D_; H = H_; Z = Z_; R1 = R1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; goto loc_f18; } } goto end; } loc_f15: { if (nondet_bool()) { int H_ = G; int D_ = 1; if (D == 1 && G == H && H >= 0 && 0 >= C && A >= 2) { D = D_; H = H_; goto loc_f27; } } if (nondet_bool()) { int Y_0 = nondet(); int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int M_ = nondet(); int G_ = nondet(); int P_ = 2; int O_ = -1 + Y_0; int N_ = -1; int H_ = -1 + G_; int D_ = 2; int C_ = -1 + Y_0; if (G >= 0 && Y_0 >= 1 && C >= 1 && A >= 2) { C = C_; D = D_; G = G_; H = H_; M = M_; N = N_; O = O_; P = P_; Q = Q_; R = R_; S = S_; goto loc_f18; } } if (nondet_bool()) { int G2_ = nondet(); int H2_ = -1; int Q1_ = 0; int O1_ = R1; int N1_ = 0; int M1_ = R1; int L1_ = 0; int I1_ = R1; int H1_ = R1; int G1_ = J1; int G_ = 0; int D_ = 1 + J1; if (D == 1 && G == 0 && Q1 == 0 && C >= 1 && A >= 2 && G2_ >= 0) { D = D_; G = G_; G1 = G1_; H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; Q1 = Q1_; G2 = G2_; H2 = H2_; goto loc_f11; } } goto end; } loc_f16: { if (nondet_bool()) { int F2_ = nondet(); int E2_ = nondet(); int Z_ = nondet(); int C_ = nondet(); int D2_ = E2; int R1_ = Q1; int A_ = 1; if (A == 1 && Q1 == R1 && 0 >= C) { A = A_; C = C_; Z = Z_; R1 = R1_; D2 = D2_; E2 = E2_; F2 = F2_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int U2_ = nondet(); int T2_ = nondet(); int S2_ = nondet(); int R2_ = nondet(); int E2_ = nondet(); int P1_ = nondet(); int O1_ = nondet(); int N1_ = nondet(); int M1_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int Q2_ = -1 + Y_0; int P2_ = -1; int R1_ = 0; int Q1_ = 0; int C_ = -1 + Y_0; int A_ = 1; if (A == 1 && R1 == 0 && Q1 == 0 && Y_0 >= 2 && C >= 1) { A = A_; C = C_; H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; Q1 = Q1_; R1 = R1_; E2 = E2_; P2 = P2_; Q2 = Q2_; R2 = R2_; S2 = S2_; T2 = T2_; U2 = U2_; goto loc_f20; } } if (nondet_bool()) { int W2_ = nondet(); int V2_ = nondet(); int S2_ = nondet(); int R2_ = nondet(); int E2_ = nondet(); int P1_ = nondet(); int O1_ = nondet(); int N1_ = nondet(); int M1_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int Q2_ = 0; int P2_ = -1; int R1_ = 0; int Q1_ = 0; int C_ = 0; int A_ = 1; if (A == 1 && R1 == 0 && Q1 == 0 && C >= 1) { A = A_; C = C_; H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; Q1 = Q1_; R1 = R1_; E2 = E2_; P2 = P2_; Q2 = Q2_; R2 = R2_; S2 = S2_; V2 = V2_; W2 = W2_; goto loc_f20; } } goto end; } loc_f18: { if (nondet_bool()) { int U_ = nondet(); int T_ = nondet(); int H_ = nondet(); int D_ = nondet(); if (0 >= C && H >= 0 && D >= 0) { D = D_; H = H_; T = T_; U = U_; goto loc_f27; } } if (nondet_bool()) { int X_ = -1 + H; int W_ = 1 + D; int H_ = -1 + H; int D_ = 1 + D; int C_ = -1 + C; if (C == V && H >= 0 && V >= 1 && D >= 0 && A >= 2) { C = C_; D = D_; H = H_; W = W_; X = X_; goto loc_f18; } } if (nondet_bool()) { int I2_ = nondet(); int G2_ = nondet(); int H2_ = -1; int Q1_ = 0; int O1_ = R1; int N1_ = 0; int M1_ = R1; int L1_ = 0; int I1_ = R1; int H1_ = R1; int G1_ = J1; int D_ = 1 + J1; if (Q1 == 0 && H >= 0 && D >= 0 && C >= 1 && A >= 2 && I2_ >= 0 && G2_ >= 0) { D = D_; G1 = G1_; H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; Q1 = Q1_; G2 = G2_; H2 = H2_; I2 = I2_; goto loc_f11; } } goto end; } loc_f19: { if (nondet_bool()) { int N2_ = nondet(); int L2_ = nondet(); int E2_ = nondet(); int E1_ = nondet(); int C1_ = nondet(); int Z_ = nondet(); int A_ = nondet(); int M2_ = 2; int A2_ = E1; int F1_ = E1; int D1_ = E1; int B_ = 2; if (E1 == A2 && C1_ >= 2) { A = A_; B = B_; Z = Z_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; A2 = A2_; E2 = E2_; L2 = L2_; M2 = M2_; N2 = N2_; goto loc_f1; } } if (nondet_bool()) { int O2_ = nondet(); int L2_ = nondet(); int F2_ = nondet(); int E2_ = nondet(); int B2_ = nondet(); int A2_ = nondet(); int P1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int Z_ = nondet(); int C_ = nondet(); int B_ = nondet(); int R1_ = E1; int Q1_ = E1; int A_ = 1; if (E1 == A2) { A = A_; B = B_; C = C_; Z = Z_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; P1 = P1_; Q1 = Q1_; R1 = R1_; A2 = A2_; B2 = B2_; E2 = E2_; F2 = F2_; L2 = L2_; O2 = O2_; goto loc_f16; } } if (nondet_bool()) { int B2_ = nondet(); int A2_ = nondet(); int P1_ = nondet(); int O1_ = nondet(); int N1_ = nondet(); int M1_ = nondet(); int L1_ = nondet(); int I1_ = nondet(); int H1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int Z_ = nondet(); int B_ = nondet(); int A_ = nondet(); int R1_ = 0; int Q1_ = 0; if (0 >= A_) { A = A_; B = B_; Z = Z_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; Q1 = Q1_; R1 = R1_; A2 = A2_; B2 = B2_; goto loc_f20; } } goto end; } loc_f27: { if (nondet_bool()) { int Z_ = nondet(); int C_ = nondet(); int B1_ = H; int A1_ = D; if (H >= 0 && 0 >= Y && D >= 0 && A >= 2) { C = C_; Z = Z_; A1 = A1_; B1 = B1_; goto loc_f18; } } if (nondet_bool()) { int J2_ = nondet(); int K2_ = -1; int T1_ = U1; int Q1_ = 0; int O1_ = R1; int N1_ = 0; int M1_ = R1; int L1_ = 0; int I1_ = R1; int H1_ = R1; int D_ = 1 + U1; if (Q1 == 0 && H >= 0 && D >= 0 && 0 >= C && A >= 2 && J2_ >= 0) { D = D_; H1 = H1_; I1 = I1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; Q1 = Q1_; T1 = T1_; J2 = J2_; K2 = K2_; goto loc_f13; } } goto end; } loc_f20: end: return 0; }