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) { goto loc_f3; loc_f113: { if (nondet_bool()) { int L1_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; L1 = L1_; goto loc_f149; } } if (nondet_bool()) { int A2_ = B1; int Z1_ = W; int Y1_ = A1; int X1_ = V; int W1_ = U; int V1_ = X; int U1_ = Z; if (Y >= 1) { U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; goto loc_f121; } } goto end; } loc_f121: { if (nondet_bool()) { int B2_ = 1; int Y_ = 1; if (Y1 >= 1) { Y = Y_; B2 = B2_; goto loc_f128; } } if (nondet_bool()) { int B2_ = 0; int Y_ = 0; if (0 >= Y1) { Y = Y_; B2 = B2_; goto loc_f128; } } goto end; } loc_f128: { if (nondet_bool()) { int Z_ = nondet(); int U_ = 11; if (Y >= 1) { U = U_; Z = Z_; goto loc_f83; } } if (nondet_bool()) { int L1_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; L1 = L1_; goto loc_f149; } } goto end; } loc_f133: { if (nondet_bool()) { int J2_ = 1; int I2_ = B1; int H2_ = W; int G2_ = A1; int F2_ = V; int E2_ = U; int D2_ = X; int C2_ = Z; int Y_ = 1; if (A1 >= 1) { Y = Y_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; goto loc_f143; } } if (nondet_bool()) { int J2_ = 0; int I2_ = B1; int H2_ = W; int G2_ = A1; int F2_ = V; int E2_ = U; int D2_ = X; int C2_ = Z; int Y_ = 0; if (0 >= A1) { Y = Y_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; goto loc_f143; } } goto end; } loc_f143: { if (nondet_bool()) { int K1_ = L1; if (Y >= 1) { K1 = K1_; goto loc_f149; } } if (nondet_bool()) { int L1_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; L1 = L1_; goto loc_f149; } } goto end; } loc_f149: { if (nondet_bool()) { int Y2_ = J; int X2_ = I; int W2_ = H; int V2_ = B; int U2_ = A; int T2_ = G; int S2_ = F; if (0 >= K1) { S2 = S2_; T2 = T2_; U2 = U2_; V2 = V2_; W2 = W2_; X2 = X2_; Y2 = Y2_; goto loc_f281; } } goto end; } loc_f15: { if (nondet_bool()) { int B_ = 0; int A_ = 3; if (1 >= 0) { A = A_; B = B_; goto loc_f22; } } goto end; } loc_f160: { if (nondet_bool()) { int L2_ = 0; int K2_ = 3; if (1 >= 0) { K2 = K2_; L2 = L2_; goto loc_f167; } } goto end; } loc_f167: { if (nondet_bool()) { int N2_ = nondet(); int M2_ = -1 + M2; int K2_ = 3; if (N2_ >= 1 && 0 >= M2) { K2 = K2_; M2 = M2_; N2 = N2_; goto loc_f167; } } if (nondet_bool()) { int N2_ = nondet(); int M2_ = -2 + M2; int K2_ = 3; if (0 >= N2_ && 0 >= M2) { K2 = K2_; M2 = M2_; N2 = N2_; goto loc_f167; } } if (nondet_bool()) { int O2_ = nondet(); int K2_ = 11; if (0 >= M2) { K2 = K2_; O2 = O2_; goto loc_f183; } } goto end; } loc_f183: { if (nondet_bool()) { int Q2_ = 1; int K2_ = 12; int J1_ = 1; int I1_ = P2; int H1_ = M2; int G1_ = 1; int F1_ = L2; int E1_ = 12; int D1_ = N2; int C1_ = O2; int Y_ = 1; if (O2 >= 1) { Y = Y_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; J1 = J1_; K2 = K2_; Q2 = Q2_; goto loc_f196; } } if (nondet_bool()) { int Q2_ = 0; int K2_ = 13; int S1_ = P2; int R1_ = M2; int Q1_ = 0; int P1_ = L2; int O1_ = 13; int N1_ = N2; int M1_ = O2; if (0 >= O2) { M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; Q1 = Q1_; R1 = R1_; S1 = S1_; K2 = K2_; Q2 = Q2_; goto loc_f206; } } goto end; } loc_f196: { if (nondet_bool()) { int R2_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; R2 = R2_; goto loc_f249; } } if (nondet_bool()) { int A2_ = P2; int Z1_ = M2; int Y1_ = Q2; int X1_ = L2; int W1_ = K2; int V1_ = N2; int U1_ = O2; if (Y >= 1) { U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; goto loc_f221; } } goto end; } loc_f206: { if (nondet_bool()) { int T1_ = 1; int Y_ = 1; if (Q1 >= 1) { Y = Y_; T1 = T1_; goto loc_f213; } } if (nondet_bool()) { int T1_ = 0; int Y_ = 0; if (0 >= Q1) { Y = Y_; T1 = T1_; goto loc_f213; } } goto end; } loc_f213: { if (nondet_bool()) { int R2_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; R2 = R2_; goto loc_f249; } } if (nondet_bool()) { int A2_ = P2; int Z1_ = M2; int Y1_ = Q2; int X1_ = L2; int W1_ = K2; int V1_ = N2; int U1_ = O2; if (Y >= 1) { U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; goto loc_f221; } } goto end; } loc_f22: { if (nondet_bool()) { int G_ = nondet(); int I_ = -1 + I; int A_ = 7; if (G_ >= 1 && 0 >= I) { A = A_; G = G_; I = I_; goto loc_f33; } } if (nondet_bool()) { int G_ = nondet(); int I_ = -2 + I; int A_ = 8; if (0 >= G_ && 0 >= I) { A = A_; G = G_; I = I_; goto loc_f33; } } if (nondet_bool()) { int F_ = nondet(); int A_ = 11; if (0 >= I) { A = A_; F = F_; goto loc_f53; } } goto end; } loc_f221: { if (nondet_bool()) { int B2_ = 1; int Y_ = 1; if (Y1 >= 1) { Y = Y_; B2 = B2_; goto loc_f228; } } if (nondet_bool()) { int B2_ = 0; int Y_ = 0; if (0 >= Y1) { Y = Y_; B2 = B2_; goto loc_f228; } } goto end; } loc_f228: { if (nondet_bool()) { int O2_ = nondet(); int K2_ = 11; if (Y >= 1) { K2 = K2_; O2 = O2_; goto loc_f183; } } if (nondet_bool()) { int R2_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; R2 = R2_; goto loc_f249; } } goto end; } loc_f233: { if (nondet_bool()) { int J2_ = 1; int I2_ = P2; int H2_ = M2; int G2_ = Q2; int F2_ = L2; int E2_ = K2; int D2_ = N2; int C2_ = O2; int Y_ = 1; if (Q2 >= 1) { Y = Y_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; goto loc_f243; } } if (nondet_bool()) { int J2_ = 0; int I2_ = P2; int H2_ = M2; int G2_ = Q2; int F2_ = L2; int E2_ = K2; int D2_ = N2; int C2_ = O2; int Y_ = 0; if (0 >= Q2) { Y = Y_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; goto loc_f243; } } goto end; } loc_f243: { if (nondet_bool()) { int K1_ = R2; if (Y >= 1) { K1 = K1_; goto loc_f249; } } if (nondet_bool()) { int R2_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; R2 = R2_; goto loc_f249; } } goto end; } loc_f249: { if (nondet_bool()) { int Y2_ = J; int X2_ = I; int W2_ = H; int V2_ = B; int U2_ = A; int T2_ = G; int S2_ = F; if (0 >= K1) { S2 = S2_; T2 = T2_; U2 = U2_; V2 = V2_; W2 = W2_; X2 = X2_; Y2 = Y2_; goto loc_f281; } } goto end; } loc_f258: { if (nondet_bool()) { int V2_ = 0; int U2_ = 3; if (1 >= 0) { U2 = U2_; V2 = V2_; goto loc_f265; } } goto end; } loc_f265: { if (nondet_bool()) { int T2_ = nondet(); int X2_ = -1 + X2; int U2_ = 3; if (T2_ >= 1 && 0 >= X2) { T2 = T2_; U2 = U2_; X2 = X2_; goto loc_f265; } } if (nondet_bool()) { int T2_ = nondet(); int X2_ = -2 + X2; int U2_ = 3; if (0 >= T2_ && 0 >= X2) { T2 = T2_; U2 = U2_; X2 = X2_; goto loc_f265; } } if (nondet_bool()) { int S2_ = nondet(); int U2_ = 11; if (0 >= X2) { S2 = S2_; U2 = U2_; goto loc_f281; } } goto end; } loc_f281: { if (nondet_bool()) { int W2_ = 1; int U2_ = 12; int J1_ = 1; int I1_ = Y2; int H1_ = X2; int G1_ = 1; int F1_ = V2; int E1_ = 12; int D1_ = T2; int C1_ = S2; int Y_ = 1; if (S2 >= 1) { Y = Y_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; J1 = J1_; U2 = U2_; W2 = W2_; goto loc_f294; } } if (nondet_bool()) { int W2_ = 0; int U2_ = 13; int T1_ = 0; int S1_ = Y2; int R1_ = X2; int Q1_ = 0; int P1_ = V2; int O1_ = 13; int N1_ = T2; int M1_ = S2; int Y_ = 0; if (0 >= S2) { Y = Y_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U2 = U2_; W2 = W2_; goto loc_f311; } } goto end; } loc_f294: { if (nondet_bool()) { int Z2_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; Z2 = Z2_; goto loc_f347; } } if (nondet_bool()) { int A2_ = Y2; int Z1_ = X2; int Y1_ = W2; int X1_ = V2; int W1_ = U2; int V1_ = T2; int U1_ = S2; if (Y >= 1) { U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; goto loc_f319; } } goto end; } loc_f3: { if (nondet_bool()) { int J_ = nondet(); int I_ = nondet(); int G_ = nondet(); int F_ = nondet(); int L_ = 0; int K_ = 0; int H_ = 0; int E_ = 0; int D_ = 0; int C_ = 0; int B_ = 0; int A_ = 3; if (1 >= 0) { A = A_; B = B_; C = C_; D = D_; E = E_; F = F_; G = G_; H = H_; I = I_; J = J_; K = K_; L = L_; goto loc_f22; } } goto end; } loc_f311: { if (nondet_bool()) { int Z2_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; Z2 = Z2_; goto loc_f347; } } if (nondet_bool()) { int A2_ = Y2; int Z1_ = X2; int Y1_ = W2; int X1_ = V2; int W1_ = U2; int V1_ = T2; int U1_ = S2; if (Y >= 1) { U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; goto loc_f319; } } goto end; } loc_f319: { if (nondet_bool()) { int B2_ = 1; int Y_ = 1; if (Y1 >= 1) { Y = Y_; B2 = B2_; goto loc_f326; } } if (nondet_bool()) { int B2_ = 0; int Y_ = 0; if (0 >= Y1) { Y = Y_; B2 = B2_; goto loc_f326; } } goto end; } loc_f326: { if (nondet_bool()) { int S2_ = nondet(); int U2_ = 11; if (Y >= 1) { S2 = S2_; U2 = U2_; goto loc_f281; } } if (nondet_bool()) { int Z2_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; Z2 = Z2_; goto loc_f347; } } goto end; } loc_f33: { if (nondet_bool()) { int M_ = nondet(); int A_ = 3; if (0 >= M_ && 0 >= L) { A = A_; M = M_; goto loc_f22; } } if (nondet_bool()) { int M_ = nondet(); int T_ = J; int S_ = I; int R_ = H; int Q_ = B; int P_ = A; int O_ = G; int N_ = F; int L_ = 1; int A_ = 3; if (M_ >= 1 && 0 >= L) { A = A_; L = L_; M = M_; N = N_; O = O_; P = P_; Q = Q_; R = R_; S = S_; T = T_; goto loc_f22; } } if (nondet_bool()) { int R3_ = 0; int Q3_ = 0; if (L >= 1) { Q3 = Q3_; R3 = R3_; goto loc_f666666; } } goto end; } loc_f331: { if (nondet_bool()) { int J2_ = 1; int I2_ = Y2; int H2_ = X2; int G2_ = W2; int F2_ = V2; int E2_ = U2; int D2_ = T2; int C2_ = S2; int Y_ = 1; if (W2 >= 1) { Y = Y_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; goto loc_f341; } } if (nondet_bool()) { int J2_ = 0; int I2_ = Y2; int H2_ = X2; int G2_ = W2; int F2_ = V2; int E2_ = U2; int D2_ = T2; int C2_ = S2; int Y_ = 0; if (0 >= W2) { Y = Y_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; goto loc_f341; } } goto end; } loc_f341: { if (nondet_bool()) { int K1_ = Z2; if (Y >= 1) { K1 = K1_; goto loc_f347; } } if (nondet_bool()) { int Z2_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; Z2 = Z2_; goto loc_f347; } } goto end; } loc_f347: { if (nondet_bool()) { int A3_ = nondet(); int F_ = nondet(); int A_ = 11; if (0 >= K1 && 0 >= K && 0 >= A3_) { A = A_; F = F_; A3 = A3_; goto loc_f53; } } if (nondet_bool()) { int A3_ = nondet(); int F_ = nondet(); int H3_ = J; int G3_ = I; int F3_ = H; int E3_ = B; int D3_ = A; int C3_ = G; int B3_ = F; int K_ = 1; int A_ = 11; if (0 >= K1 && 0 >= K && A3_ >= 1) { A = A_; F = F_; K = K_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; E3 = E3_; F3 = F3_; G3 = G3_; H3 = H3_; goto loc_f53; } } if (nondet_bool()) { int R3_ = 0; int Q3_ = 0; if (0 >= K1 && K >= 1) { Q3 = Q3_; R3 = R3_; goto loc_f666666; } } goto end; } loc_f367: { if (nondet_bool()) { int M3_ = nondet(); int O3_ = J; int N3_ = H; int L3_ = G; int K3_ = I; int J3_ = B; int I3_ = 11; if (1 >= 0) { I3 = I3_; J3 = J3_; K3 = K3_; L3 = L3_; M3 = M3_; N3 = N3_; O3 = O3_; goto loc_f394; } } goto end; } loc_f371: { if (nondet_bool()) { int J3_ = 0; int I3_ = 3; if (1 >= 0) { I3 = I3_; J3 = J3_; goto loc_f378; } } goto end; } loc_f378: { if (nondet_bool()) { int L3_ = nondet(); int K3_ = -1 + K3; int I3_ = 3; if (L3_ >= 1 && 0 >= K3) { I3 = I3_; K3 = K3_; L3 = L3_; goto loc_f378; } } if (nondet_bool()) { int L3_ = nondet(); int K3_ = -2 + K3; int I3_ = 3; if (0 >= L3_ && 0 >= K3) { I3 = I3_; K3 = K3_; L3 = L3_; goto loc_f378; } } if (nondet_bool()) { int M3_ = nondet(); int I3_ = 11; if (0 >= K3) { I3 = I3_; M3 = M3_; goto loc_f394; } } goto end; } loc_f394: { if (nondet_bool()) { int N3_ = 1; int I3_ = 12; int J1_ = 1; int I1_ = O3; int H1_ = K3; int G1_ = 1; int F1_ = J3; int E1_ = 12; int D1_ = L3; int C1_ = M3; int Y_ = 1; if (M3 >= 1) { Y = Y_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; J1 = J1_; I3 = I3_; N3 = N3_; goto loc_f407; } } if (nondet_bool()) { int N3_ = 0; int I3_ = 13; int T1_ = 0; int S1_ = O3; int R1_ = K3; int Q1_ = 0; int P1_ = J3; int O1_ = 13; int N1_ = L3; int M1_ = M3; int Y_ = 0; if (0 >= M3) { Y = Y_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; I3 = I3_; N3 = N3_; goto loc_f424; } } goto end; } loc_f407: { if (nondet_bool()) { int P3_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; P3 = P3_; goto loc_f460; } } if (nondet_bool()) { int A2_ = O3; int Z1_ = K3; int Y1_ = N3; int X1_ = J3; int W1_ = I3; int V1_ = L3; int U1_ = M3; if (Y >= 1) { U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; goto loc_f432; } } goto end; } loc_f424: { if (nondet_bool()) { int P3_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; P3 = P3_; goto loc_f460; } } if (nondet_bool()) { int A2_ = O3; int Z1_ = K3; int Y1_ = N3; int X1_ = J3; int W1_ = I3; int V1_ = L3; int U1_ = M3; if (Y >= 1) { U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; goto loc_f432; } } goto end; } loc_f432: { if (nondet_bool()) { int B2_ = 1; int Y_ = 1; if (Y1 >= 1) { Y = Y_; B2 = B2_; goto loc_f439; } } if (nondet_bool()) { int B2_ = 0; int Y_ = 0; if (0 >= Y1) { Y = Y_; B2 = B2_; goto loc_f439; } } goto end; } loc_f439: { if (nondet_bool()) { int M3_ = nondet(); int I3_ = 11; if (Y >= 1) { I3 = I3_; M3 = M3_; goto loc_f394; } } if (nondet_bool()) { int P3_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; P3 = P3_; goto loc_f460; } } goto end; } loc_f444: { if (nondet_bool()) { int J2_ = 1; int I2_ = O3; int H2_ = K3; int G2_ = N3; int F2_ = J3; int E2_ = I3; int D2_ = L3; int C2_ = M3; int Y_ = 1; if (N3 >= 1) { Y = Y_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; goto loc_f454; } } if (nondet_bool()) { int J2_ = 0; int I2_ = O3; int H2_ = K3; int G2_ = N3; int F2_ = J3; int E2_ = I3; int D2_ = L3; int C2_ = M3; int Y_ = 0; if (0 >= N3) { Y = Y_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; goto loc_f454; } } goto end; } loc_f454: { if (nondet_bool()) { int K1_ = P3; if (Y >= 1) { K1 = K1_; goto loc_f460; } } if (nondet_bool()) { int P3_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; P3 = P3_; goto loc_f460; } } goto end; } loc_f460: { if (nondet_bool()) { int R3_ = Q3; if (0 >= K1 && Q3 >= 2) { R3 = R3_; goto loc_f666666; } } if (nondet_bool()) { int R3_ = Q3; if (0 >= K1 && 0 >= Q3) { R3 = R3_; goto loc_f666666; } } goto end; } loc_f53: { if (nondet_bool()) { int I1_ = J; int H1_ = I; int G1_ = 1; int F1_ = B; int E1_ = 12; int D1_ = G; int C1_ = F; int B1_ = J; int A1_ = 1; int Z_ = F; int X_ = G; int W_ = I; int V_ = B; int U_ = 12; int H_ = 1; int A_ = 12; if (F >= 1) { A = A_; H = H_; U = U_; V = V_; W = W_; X = X_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f89; } } if (nondet_bool()) { int Q2_ = 0; int P2_ = J; int O2_ = F; int N2_ = G; int M2_ = I; int L2_ = B; int K2_ = 13; int S1_ = J; int R1_ = I; int Q1_ = 0; int P1_ = B; int O1_ = 13; int N1_ = G; int M1_ = F; int H_ = 0; int A_ = 13; if (0 >= F) { A = A_; H = H_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; Q1 = Q1_; R1 = R1_; S1 = S1_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; O2 = O2_; P2 = P2_; Q2 = Q2_; goto loc_f206; } } goto end; } loc_f60: { if (nondet_bool()) { int V_ = 0; int U_ = 3; if (1 >= 0) { U = U_; V = V_; goto loc_f67; } } goto end; } loc_f67: { if (nondet_bool()) { int X_ = nondet(); int W_ = -1 + W; int U_ = 3; if (X_ >= 1 && 0 >= W) { U = U_; W = W_; X = X_; goto loc_f67; } } if (nondet_bool()) { int X_ = nondet(); int W_ = -2 + W; int U_ = 3; if (0 >= X_ && 0 >= W) { U = U_; W = W_; X = X_; goto loc_f67; } } if (nondet_bool()) { int Z_ = nondet(); int U_ = 11; if (0 >= W) { U = U_; Z = Z_; goto loc_f83; } } goto end; } loc_f83: { if (nondet_bool()) { int I1_ = B1; int H1_ = W; int G1_ = 1; int F1_ = V; int E1_ = 12; int D1_ = X; int C1_ = Z; int A1_ = 1; int U_ = 12; if (Z >= 1) { U = U_; A1 = A1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f89; } } if (nondet_bool()) { int T1_ = 0; int S1_ = B1; int R1_ = W; int Q1_ = 0; int P1_ = V; int O1_ = 13; int N1_ = X; int M1_ = Z; int A1_ = 0; int Y_ = 0; int U_ = 13; if (0 >= Z) { U = U_; Y = Y_; A1 = A1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; goto loc_f113; } } goto end; } loc_f89: { if (nondet_bool()) { int J1_ = 1; int Y_ = 1; if (G1 >= 1) { Y = Y_; J1 = J1_; goto loc_f96; } } if (nondet_bool()) { int J1_ = 0; int Y_ = 0; if (0 >= G1) { Y = Y_; J1 = J1_; goto loc_f96; } } goto end; } loc_f96: { if (nondet_bool()) { int L1_ = 0; int K1_ = 0; if (0 >= Y) { K1 = K1_; L1 = L1_; goto loc_f149; } } if (nondet_bool()) { int A2_ = B1; int Z1_ = W; int Y1_ = A1; int X1_ = V; int W1_ = U; int V1_ = X; int U1_ = Z; if (Y >= 1) { U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; goto loc_f121; } } goto end; } loc_f666666: end: return 0; }