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, int B6, int C6, int D6, int E6, int F6, int G6, int H6, int I6, int J6, int K6, int L6, int M6, int N6, int O6, int P6, int Q6, int R6, int S6, int T6, int U6, int V6, int W6, int X6, int Y6, int Z6, int A7, int B7, int C7, int D7, int E7, int F7, int G7, int H7, int I7, int J7, int K7, int L7, int M7, int N7, int O7, int P7, int Q7, int R7, int S7, int T7, int U7, int V7) { goto loc_f3; loc_f134: { if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f193; } } if (nondet_bool()) { int S_ = 8; if (0 >= B) { S = S_; goto loc_f144; } } goto end; } loc_f144: { if (nondet_bool()) { int H1_ = 0; int U_ = -1 + U; int S_ = 10; int C_ = 0; if (X >= 1 && U >= 0 && H >= 1) { C = C_; S = S_; U = U_; H1 = H1_; goto loc_f193; } } if (nondet_bool()) { int O2_ = nondet(); int U_ = -1 + U; int S_ = 8; if (0 >= O2_ && U >= 0 && 0 >= X) { S = S_; U = U_; O2 = O2_; goto loc_f144; } } if (nondet_bool()) { int O2_ = nondet(); int V2_ = W; int U2_ = V; int T2_ = -1 + U; int S2_ = T; int R2_ = 10; int Q2_ = R; int P2_ = Q; int X_ = 1; int U_ = -1 + U; int S_ = 8; if (O2_ >= 1 && U >= 0 && 0 >= X && 0 >= Y) { S = S_; U = U_; X = X_; O2 = O2_; P2 = P2_; Q2 = Q2_; R2 = R2_; S2 = S2_; T2 = T2_; U2 = U2_; V2 = V2_; goto loc_f144; } } if (nondet_bool()) { int T_ = 1; int S_ = 11; if (0 >= A && 0 >= 1 + U) { S = S_; T = T_; goto loc_f179; } } if (nondet_bool()) { int D3_ = 1; int C3_ = W; int B3_ = V; int A3_ = U; int Z2_ = 1; int Y2_ = 11; int X2_ = R; int W2_ = Q; int T_ = 1; int S_ = 11; int B_ = 1; if (A >= 1 && 0 >= 1 + U) { B = B_; S = S_; T = T_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; goto loc_f179; } } goto end; } loc_f17: { if (nondet_bool()) { int D_ = nondet(); int E_ = 2; if (1 >= 0) { D = D_; E = E_; goto loc_f22; } } goto end; } loc_f179: { if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f193; } } if (nondet_bool()) { int S_ = 14; if (0 >= B) { S = S_; goto loc_f191; } } goto end; } loc_f191: { if (nondet_bool()) { int S_ = 14; if (1 >= 0) { S = S_; goto loc_f191; } } goto end; } loc_f193: { if (nondet_bool()) { if (0 >= C) { goto loc_f200; } } goto end; } loc_f200: { if (nondet_bool()) { if (0 >= A) { goto loc_f362; } } if (nondet_bool()) { int M3_ = 0; int L3_ = 0; int K3_ = N; int J3_ = M; int I3_ = L; int H3_ = K; int G3_ = E; int F3_ = D; int E3_ = J; if (A >= 1) { E3 = E3_; F3 = F3_; G3 = G3_; H3 = H3_; I3 = I3_; J3 = J3_; K3 = K3_; L3 = L3_; M3 = M3_; goto loc_f216; } } goto end; } loc_f207: { if (nondet_bool()) { int F3_ = nondet(); int G3_ = 2; if (1 >= 0) { F3 = F3_; G3 = G3_; goto loc_f212; } } goto end; } loc_f212: { if (nondet_bool()) { int G3_ = 4; if (J3 >= 0) { G3 = G3_; goto loc_f216; } } if (nondet_bool()) { int G3_ = 3; if (0 >= 1 + J3 && 0 >= A) { G3 = G3_; goto loc_f303; } } if (nondet_bool()) { int G3_ = 3; int N2_ = 1; int M2_ = K3; int L2_ = J3; int K2_ = I3; int J2_ = H3; int I2_ = 3; int H2_ = F3; int G2_ = E3; int B_ = 1; if (H3 >= 1 && A >= 1 && 0 >= 1 + J3) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; G3 = G3_; goto loc_f303; } } if (nondet_bool()) { int G3_ = 3; int N2_ = 0; int M2_ = K3; int L2_ = J3; int K2_ = I3; int J2_ = H3; int I2_ = 3; int H2_ = F3; int G2_ = E3; int B_ = 0; if (0 >= H3 && A >= 1 && 0 >= 1 + J3) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; G3 = G3_; goto loc_f303; } } goto end; } loc_f216: { if (nondet_bool()) { int J3_ = -1 + J3; int G3_ = 5; if (F3 >= 1) { G3 = G3_; J3 = J3_; goto loc_f239; } } if (nondet_bool()) { int H3_ = 0; int G3_ = 6; if (0 >= F3 && 0 >= A) { G3 = G3_; H3 = H3_; goto loc_f232; } } if (nondet_bool()) { int H3_ = 0; int G3_ = 6; int G1_ = 0; int F1_ = K3; int E1_ = J3; int D1_ = I3; int C1_ = 0; int B1_ = 6; int A1_ = F3; int Z_ = E3; int B_ = 0; if (0 >= F3 && A >= 1) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; G3 = G3_; H3 = H3_; goto loc_f232; } } goto end; } loc_f22: { if (nondet_bool()) { int E_ = 3; if (0 >= A && 0 >= 1 + M) { E = E_; goto loc_f717; } } if (nondet_bool()) { int M_ = -1 + M; int E_ = 5; if (D >= 1 && M >= 0) { E = E_; M = M_; goto loc_f200; } } if (nondet_bool()) { int K_ = 0; int E_ = 6; if (0 >= A && M >= 0 && 0 >= D) { E = E_; K = K_; goto loc_f193; } } if (nondet_bool()) { int Y_ = 0; int X_ = 0; int W_ = N; int V_ = M; int U_ = L; int T_ = 0; int S_ = 6; int R_ = D; int Q_ = J; int K_ = 0; int E_ = 6; if (A >= 1 && M >= 0 && 0 >= D) { E = E_; K = K_; Q = Q_; R = R_; S = S_; T = T_; U = U_; V = V_; W = W_; X = X_; Y = Y_; goto loc_f52; } } if (nondet_bool()) { int M5_ = nondet(); int U5_ = 0; int T5_ = 0; int S5_ = N; int R5_ = M; int Q5_ = L; int P5_ = K; int O5_ = J; int N5_ = 2; int E_ = 3; if (A >= 1 && 0 >= 1 + M) { E = E_; M5 = M5_; N5 = N5_; O5 = O5_; P5 = P5_; Q5 = Q5_; R5 = R5_; S5 = S5_; T5 = T5_; U5 = U5_; goto loc_f567; } } goto end; } loc_f232: { if (nondet_bool()) { if (0 >= B) { goto loc_f239; } } if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f362; } } goto end; } loc_f239: { if (nondet_bool()) { if (0 >= A) { goto loc_f250; } } if (nondet_bool()) { int P1_ = 1; int O1_ = K3; int N1_ = J3; int M1_ = I3; int L1_ = H3; int K1_ = G3; int J1_ = F3; int I1_ = E3; int B_ = 1; if (H3 >= 1 && A >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f250; } } if (nondet_bool()) { int P1_ = 0; int O1_ = K3; int N1_ = J3; int M1_ = I3; int L1_ = H3; int K1_ = G3; int J1_ = F3; int I1_ = E3; int B_ = 0; if (0 >= H3 && A >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f250; } } goto end; } loc_f250: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f268; } } if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f362; } } if (nondet_bool()) { int X1_ = 1; int W1_ = K3; int V1_ = J3; int U1_ = I3; int T1_ = H3; int S1_ = G3; int R1_ = F3; int Q1_ = E3; int B_ = 1; if (0 >= B && A >= 1 && H3 >= 1) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f268; } } if (nondet_bool()) { int X1_ = 0; int W1_ = K3; int V1_ = J3; int U1_ = I3; int T1_ = H3; int S1_ = G3; int R1_ = F3; int Q1_ = E3; int B_ = 0; if (0 >= B && A >= 1 && 0 >= H3) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f268; } } goto end; } loc_f268: { if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f362; } } if (nondet_bool()) { int N3_ = 0; int C_ = 0; if (0 >= B && H >= 1 && M3 >= 1) { C = C_; N3 = N3_; goto loc_f362; } } if (nondet_bool()) { int O3_ = nondet(); int F3_ = nondet(); int G3_ = 2; if (0 >= B && 0 >= O3_ && 0 >= M3) { F3 = F3_; G3 = G3_; O3 = O3_; goto loc_f212; } } if (nondet_bool()) { int O3_ = nondet(); int F3_ = nondet(); int V3_ = K3; int U3_ = J3; int T3_ = I3; int S3_ = H3; int R3_ = G3; int Q3_ = F3; int P3_ = E3; int M3_ = 1; int G3_ = 2; if (0 >= B && O3_ >= 1 && 0 >= L3 && 0 >= M3) { F3 = F3_; G3 = G3_; M3 = M3_; O3 = O3_; P3 = P3_; Q3 = Q3_; R3 = R3_; S3 = S3_; T3 = T3_; U3 = U3_; V3 = V3_; goto loc_f212; } } goto end; } loc_f3: { if (nondet_bool()) { int N_ = nondet(); int L_ = nondet(); int J_ = nondet(); int D_ = nondet(); int P_ = 0; int O_ = 0; int M_ = 5; int K_ = 0; int I_ = 0; int H_ = 1; int G_ = 5; int F_ = 0; int E_ = 2; int A_ = 1; if (1 >= 0) { A = A_; D = D_; E = E_; F = F_; G = G_; H = H_; I = I_; J = J_; K = K_; L = L_; M = M_; N = N_; O = O_; P = P_; goto loc_f22; } } goto end; } loc_f303: { if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f362; } } if (nondet_bool()) { int G3_ = 8; if (0 >= B) { G3 = G3_; goto loc_f313; } } goto end; } loc_f313: { if (nondet_bool()) { int N3_ = 0; int I3_ = -1 + I3; int G3_ = 10; int C_ = 0; if (I3 >= 0 && H >= 1 && L3 >= 1) { C = C_; G3 = G3_; I3 = I3_; N3 = N3_; goto loc_f362; } } if (nondet_bool()) { int W3_ = nondet(); int I3_ = -1 + I3; int G3_ = 8; if (I3 >= 0 && 0 >= W3_ && 0 >= L3) { G3 = G3_; I3 = I3_; W3 = W3_; goto loc_f313; } } if (nondet_bool()) { int W3_ = nondet(); int D4_ = K3; int C4_ = J3; int B4_ = -1 + I3; int A4_ = H3; int Z3_ = 10; int Y3_ = F3; int X3_ = E3; int L3_ = 1; int I3_ = -1 + I3; int G3_ = 8; if (I3 >= 0 && W3_ >= 1 && 0 >= L3 && 0 >= M3) { G3 = G3_; I3 = I3_; L3 = L3_; W3 = W3_; X3 = X3_; Y3 = Y3_; Z3 = Z3_; A4 = A4_; B4 = B4_; C4 = C4_; D4 = D4_; goto loc_f313; } } if (nondet_bool()) { int H3_ = 1; int G3_ = 11; if (0 >= 1 + I3 && 0 >= A) { G3 = G3_; H3 = H3_; goto loc_f348; } } if (nondet_bool()) { int H3_ = 1; int G3_ = 11; int D3_ = 1; int C3_ = K3; int B3_ = J3; int A3_ = I3; int Z2_ = 1; int Y2_ = 11; int X2_ = F3; int W2_ = E3; int B_ = 1; if (0 >= 1 + I3 && A >= 1) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; G3 = G3_; H3 = H3_; goto loc_f348; } } goto end; } loc_f348: { if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f362; } } if (nondet_bool()) { int G3_ = 14; if (0 >= B) { G3 = G3_; goto loc_f360; } } goto end; } loc_f360: { if (nondet_bool()) { int G3_ = 14; if (1 >= 0) { G3 = G3_; goto loc_f360; } } goto end; } loc_f362: { if (nondet_bool()) { if (0 >= C && 0 >= A) { goto loc_f531; } } if (nondet_bool()) { int M4_ = 0; int L4_ = 0; int K4_ = N; int J4_ = M; int I4_ = L; int H4_ = K; int G4_ = E; int F4_ = D; int E4_ = J; if (0 >= C && A >= 1) { E4 = E4_; F4 = F4_; G4 = G4_; H4 = H4_; I4 = I4_; J4 = J4_; K4 = K4_; L4 = L4_; M4 = M4_; goto loc_f381; } } goto end; } loc_f376: { if (nondet_bool()) { int F4_ = nondet(); int G4_ = 2; if (1 >= 0) { F4 = F4_; G4 = G4_; goto loc_f381; } } goto end; } loc_f38: { if (nondet_bool()) { int R_ = nondet(); int S_ = 2; if (1 >= 0) { R = R_; S = S_; goto loc_f43; } } goto end; } loc_f381: { if (nondet_bool()) { int G4_ = 3; if (0 >= A && 0 >= 1 + J4) { G4 = G4_; goto loc_f472; } } if (nondet_bool()) { int J4_ = -1 + J4; int G4_ = 5; if (J4 >= 0 && F4 >= 1) { G4 = G4_; J4 = J4_; goto loc_f408; } } if (nondet_bool()) { int H4_ = 0; int G4_ = 6; if (J4 >= 0 && 0 >= F4 && 0 >= A) { G4 = G4_; H4 = H4_; goto loc_f401; } } if (nondet_bool()) { int H4_ = 0; int G4_ = 6; int G1_ = 0; int F1_ = K4; int E1_ = J4; int D1_ = I4; int C1_ = 0; int B1_ = 6; int A1_ = F4; int Z_ = E4; int B_ = 0; if (J4 >= 0 && 0 >= F4 && A >= 1) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; G4 = G4_; H4 = H4_; goto loc_f401; } } if (nondet_bool()) { int G4_ = 3; int N2_ = 1; int M2_ = K4; int L2_ = J4; int K2_ = I4; int J2_ = H4; int I2_ = 3; int H2_ = F4; int G2_ = E4; int B_ = 1; if (0 >= 1 + J4 && H4 >= 1 && A >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; G4 = G4_; goto loc_f472; } } if (nondet_bool()) { int G4_ = 3; int N2_ = 0; int M2_ = K4; int L2_ = J4; int K2_ = I4; int J2_ = H4; int I2_ = 3; int H2_ = F4; int G2_ = E4; int B_ = 0; if (0 >= 1 + J4 && 0 >= H4 && A >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; G4 = G4_; goto loc_f472; } } goto end; } loc_f401: { if (nondet_bool()) { if (0 >= B) { goto loc_f408; } } if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f531; } } goto end; } loc_f408: { if (nondet_bool()) { if (0 >= A) { goto loc_f419; } } if (nondet_bool()) { int P1_ = 1; int O1_ = K4; int N1_ = J4; int M1_ = I4; int L1_ = H4; int K1_ = G4; int J1_ = F4; int I1_ = E4; int B_ = 1; if (A >= 1 && H4 >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f419; } } if (nondet_bool()) { int P1_ = 0; int O1_ = K4; int N1_ = J4; int M1_ = I4; int L1_ = H4; int K1_ = G4; int J1_ = F4; int I1_ = E4; int B_ = 0; if (A >= 1 && 0 >= H4) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f419; } } goto end; } loc_f419: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f437; } } if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f531; } } if (nondet_bool()) { int X1_ = 1; int W1_ = K4; int V1_ = J4; int U1_ = I4; int T1_ = H4; int S1_ = G4; int R1_ = F4; int Q1_ = E4; int B_ = 1; if (A >= 1 && H4 >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f437; } } if (nondet_bool()) { int X1_ = 0; int W1_ = K4; int V1_ = J4; int U1_ = I4; int T1_ = H4; int S1_ = G4; int R1_ = F4; int Q1_ = E4; int B_ = 0; if (A >= 1 && 0 >= H4 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f437; } } goto end; } loc_f43: { if (nondet_bool()) { int S_ = 3; if (0 >= A && 0 >= 1 + V) { S = S_; goto loc_f134; } } if (nondet_bool()) { int T_ = 0; int S_ = 6; if (V >= 0 && 0 >= R) { S = S_; T = T_; goto loc_f52; } } if (nondet_bool()) { int V_ = -1 + V; int S_ = 5; if (V >= 0 && R >= 1) { S = S_; V = V_; goto loc_f70; } } if (nondet_bool()) { int N2_ = 1; int M2_ = W; int L2_ = V; int K2_ = U; int J2_ = T; int I2_ = 3; int H2_ = R; int G2_ = Q; int S_ = 3; int B_ = 1; if (0 >= 1 + V && T >= 1 && A >= 1) { B = B_; S = S_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; goto loc_f134; } } if (nondet_bool()) { int N2_ = 0; int M2_ = W; int L2_ = V; int K2_ = U; int J2_ = T; int I2_ = 3; int H2_ = R; int G2_ = Q; int S_ = 3; int B_ = 0; if (0 >= 1 + V && 0 >= T && A >= 1) { B = B_; S = S_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; goto loc_f134; } } goto end; } loc_f437: { if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f531; } } if (nondet_bool()) { int N4_ = 0; int C_ = 0; if (H >= 1 && M4 >= 1 && 0 >= B) { C = C_; N4 = N4_; goto loc_f531; } } if (nondet_bool()) { int O4_ = nondet(); int F4_ = nondet(); int G4_ = 2; if (0 >= O4_ && 0 >= M4 && 0 >= B) { F4 = F4_; G4 = G4_; O4 = O4_; goto loc_f381; } } if (nondet_bool()) { int O4_ = nondet(); int F4_ = nondet(); int V4_ = K4; int U4_ = J4; int T4_ = I4; int S4_ = H4; int R4_ = G4; int Q4_ = F4; int P4_ = E4; int M4_ = 1; int G4_ = 2; if (0 >= M4 && 0 >= L4 && O4_ >= 1 && 0 >= B) { F4 = F4_; G4 = G4_; M4 = M4_; O4 = O4_; P4 = P4_; Q4 = Q4_; R4 = R4_; S4 = S4_; T4 = T4_; U4 = U4_; V4 = V4_; goto loc_f381; } } goto end; } loc_f472: { if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f531; } } if (nondet_bool()) { int G4_ = 8; if (0 >= B) { G4 = G4_; goto loc_f482; } } goto end; } loc_f482: { if (nondet_bool()) { int N4_ = 0; int I4_ = -1 + I4; int G4_ = 10; int C_ = 0; if (L4 >= 1 && I4 >= 0 && H >= 1) { C = C_; G4 = G4_; I4 = I4_; N4 = N4_; goto loc_f531; } } if (nondet_bool()) { int W4_ = nondet(); int I4_ = -1 + I4; int G4_ = 8; if (0 >= L4 && I4 >= 0 && 0 >= W4_) { G4 = G4_; I4 = I4_; W4 = W4_; goto loc_f482; } } if (nondet_bool()) { int W4_ = nondet(); int D5_ = K4; int C5_ = J4; int B5_ = -1 + I4; int A5_ = H4; int Z4_ = 10; int Y4_ = F4; int X4_ = E4; int L4_ = 1; int I4_ = -1 + I4; int G4_ = 8; if (0 >= L4 && I4 >= 0 && 0 >= M4 && W4_ >= 1) { G4 = G4_; I4 = I4_; L4 = L4_; W4 = W4_; X4 = X4_; Y4 = Y4_; Z4 = Z4_; A5 = A5_; B5 = B5_; C5 = C5_; D5 = D5_; goto loc_f482; } } if (nondet_bool()) { int H4_ = 1; int G4_ = 11; if (0 >= A && 0 >= 1 + I4) { G4 = G4_; H4 = H4_; goto loc_f517; } } if (nondet_bool()) { int H4_ = 1; int G4_ = 11; int D3_ = 1; int C3_ = K4; int B3_ = J4; int A3_ = I4; int Z2_ = 1; int Y2_ = 11; int X2_ = F4; int W2_ = E4; int B_ = 1; if (A >= 1 && 0 >= 1 + I4) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; G4 = G4_; H4 = H4_; goto loc_f517; } } goto end; } loc_f517: { if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f531; } } if (nondet_bool()) { int G4_ = 14; if (0 >= B) { G4 = G4_; goto loc_f529; } } goto end; } loc_f52: { if (nondet_bool()) { if (0 >= A) { goto loc_f63; } } if (nondet_bool()) { int G1_ = 1; int F1_ = W; int E1_ = V; int D1_ = U; int C1_ = T; int B1_ = S; int A1_ = R; int Z_ = Q; int B_ = 1; if (A >= 1 && T >= 1) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f63; } } if (nondet_bool()) { int G1_ = 0; int F1_ = W; int E1_ = V; int D1_ = U; int C1_ = T; int B1_ = S; int A1_ = R; int Z_ = Q; int B_ = 0; if (A >= 1 && 0 >= T) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f63; } } goto end; } loc_f529: { if (nondet_bool()) { int G4_ = 14; if (1 >= 0) { G4 = G4_; goto loc_f529; } } goto end; } loc_f531: { if (nondet_bool()) { int E5_ = nondet(); int D_ = nondet(); int E_ = 2; if (0 >= E5_ && 0 >= P && 0 >= C) { D = D_; E = E_; E5 = E5_; goto loc_f22; } } if (nondet_bool()) { int E5_ = nondet(); int D_ = nondet(); int L5_ = N; int K5_ = M; int J5_ = L; int I5_ = K; int H5_ = E; int G5_ = D; int F5_ = J; int P_ = 1; int E_ = 2; if (0 >= P && 0 >= O && E5_ >= 1 && 0 >= C) { D = D_; E = E_; P = P_; E5 = E5_; F5 = F5_; G5 = G5_; H5 = H5_; I5 = I5_; J5 = J5_; K5 = K5_; L5 = L5_; goto loc_f22; } } if (nondet_bool()) { int V7_ = 0; int U7_ = 0; if (H >= 1 && P >= 1 && 0 >= C) { U7 = U7_; V7 = V7_; goto loc_f666666; } } goto end; } loc_f562: { if (nondet_bool()) { int M5_ = nondet(); int N5_ = 2; if (1 >= 0) { M5 = M5_; N5 = N5_; goto loc_f567; } } goto end; } loc_f567: { if (nondet_bool()) { int N5_ = 3; if (0 >= A && 0 >= 1 + R5) { N5 = N5_; goto loc_f658; } } if (nondet_bool()) { int R5_ = -1 + R5; int N5_ = 5; if (R5 >= 0 && M5 >= 1) { N5 = N5_; R5 = R5_; goto loc_f594; } } if (nondet_bool()) { int P5_ = 0; int N5_ = 6; if (R5 >= 0 && 0 >= M5 && 0 >= A) { N5 = N5_; P5 = P5_; goto loc_f587; } } if (nondet_bool()) { int P5_ = 0; int N5_ = 6; int G1_ = 0; int F1_ = S5; int E1_ = R5; int D1_ = Q5; int C1_ = 0; int B1_ = 6; int A1_ = M5; int Z_ = O5; int B_ = 0; if (R5 >= 0 && 0 >= M5 && A >= 1) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; N5 = N5_; P5 = P5_; goto loc_f587; } } if (nondet_bool()) { int N5_ = 3; int N2_ = 1; int M2_ = S5; int L2_ = R5; int K2_ = Q5; int J2_ = P5; int I2_ = 3; int H2_ = M5; int G2_ = O5; int B_ = 1; if (0 >= 1 + R5 && P5 >= 1 && A >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; N5 = N5_; goto loc_f658; } } if (nondet_bool()) { int N5_ = 3; int N2_ = 0; int M2_ = S5; int L2_ = R5; int K2_ = Q5; int J2_ = P5; int I2_ = 3; int H2_ = M5; int G2_ = O5; int B_ = 0; if (0 >= 1 + R5 && 0 >= P5 && A >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; N5 = N5_; goto loc_f658; } } goto end; } loc_f587: { if (nondet_bool()) { if (0 >= B) { goto loc_f594; } } if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f717; } } goto end; } loc_f594: { if (nondet_bool()) { if (0 >= A) { goto loc_f605; } } if (nondet_bool()) { int P1_ = 1; int O1_ = S5; int N1_ = R5; int M1_ = Q5; int L1_ = P5; int K1_ = N5; int J1_ = M5; int I1_ = O5; int B_ = 1; if (A >= 1 && P5 >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f605; } } if (nondet_bool()) { int P1_ = 0; int O1_ = S5; int N1_ = R5; int M1_ = Q5; int L1_ = P5; int K1_ = N5; int J1_ = M5; int I1_ = O5; int B_ = 0; if (A >= 1 && 0 >= P5) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f605; } } goto end; } loc_f605: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f623; } } if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f717; } } if (nondet_bool()) { int X1_ = 1; int W1_ = S5; int V1_ = R5; int U1_ = Q5; int T1_ = P5; int S1_ = N5; int R1_ = M5; int Q1_ = O5; int B_ = 1; if (A >= 1 && P5 >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f623; } } if (nondet_bool()) { int X1_ = 0; int W1_ = S5; int V1_ = R5; int U1_ = Q5; int T1_ = P5; int S1_ = N5; int R1_ = M5; int Q1_ = O5; int B_ = 0; if (A >= 1 && 0 >= P5 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f623; } } goto end; } loc_f623: { if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f717; } } if (nondet_bool()) { int V5_ = 0; int C_ = 0; if (H >= 1 && U5 >= 1 && 0 >= B) { C = C_; V5 = V5_; goto loc_f717; } } if (nondet_bool()) { int W5_ = nondet(); int M5_ = nondet(); int N5_ = 2; if (0 >= W5_ && 0 >= U5 && 0 >= B) { M5 = M5_; N5 = N5_; W5 = W5_; goto loc_f567; } } if (nondet_bool()) { int W5_ = nondet(); int M5_ = nondet(); int D6_ = S5; int C6_ = R5; int B6_ = Q5; int A6_ = P5; int Z5_ = N5; int Y5_ = M5; int X5_ = O5; int U5_ = 1; int N5_ = 2; if (0 >= U5 && 0 >= T5 && W5_ >= 1 && 0 >= B) { M5 = M5_; N5 = N5_; U5 = U5_; W5 = W5_; X5 = X5_; Y5 = Y5_; Z5 = Z5_; A6 = A6_; B6 = B6_; C6 = C6_; D6 = D6_; goto loc_f567; } } goto end; } loc_f63: { if (nondet_bool()) { if (0 >= B) { goto loc_f70; } } if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f193; } } goto end; } loc_f658: { if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f717; } } if (nondet_bool()) { int N5_ = 8; if (0 >= B) { N5 = N5_; goto loc_f668; } } goto end; } loc_f668: { if (nondet_bool()) { int V5_ = 0; int Q5_ = -1 + Q5; int N5_ = 10; int C_ = 0; if (T5 >= 1 && Q5 >= 0 && H >= 1) { C = C_; N5 = N5_; Q5 = Q5_; V5 = V5_; goto loc_f717; } } if (nondet_bool()) { int E6_ = nondet(); int Q5_ = -1 + Q5; int N5_ = 8; if (0 >= T5 && Q5 >= 0 && 0 >= E6_) { N5 = N5_; Q5 = Q5_; E6 = E6_; goto loc_f668; } } if (nondet_bool()) { int E6_ = nondet(); int L6_ = S5; int K6_ = R5; int J6_ = -1 + Q5; int I6_ = P5; int H6_ = 10; int G6_ = M5; int F6_ = O5; int T5_ = 1; int Q5_ = -1 + Q5; int N5_ = 8; if (0 >= T5 && Q5 >= 0 && 0 >= U5 && E6_ >= 1) { N5 = N5_; Q5 = Q5_; T5 = T5_; E6 = E6_; F6 = F6_; G6 = G6_; H6 = H6_; I6 = I6_; J6 = J6_; K6 = K6_; L6 = L6_; goto loc_f668; } } if (nondet_bool()) { int P5_ = 1; int N5_ = 11; if (0 >= A && 0 >= 1 + Q5) { N5 = N5_; P5 = P5_; goto loc_f703; } } if (nondet_bool()) { int P5_ = 1; int N5_ = 11; int D3_ = 1; int C3_ = S5; int B3_ = R5; int A3_ = Q5; int Z2_ = 1; int Y2_ = 11; int X2_ = M5; int W2_ = O5; int B_ = 1; if (A >= 1 && 0 >= 1 + Q5) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; N5 = N5_; P5 = P5_; goto loc_f703; } } goto end; } loc_f70: { if (nondet_bool()) { if (0 >= A) { goto loc_f81; } } if (nondet_bool()) { int P1_ = 1; int O1_ = W; int N1_ = V; int M1_ = U; int L1_ = T; int K1_ = S; int J1_ = R; int I1_ = Q; int B_ = 1; if (A >= 1 && T >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f81; } } if (nondet_bool()) { int P1_ = 0; int O1_ = W; int N1_ = V; int M1_ = U; int L1_ = T; int K1_ = S; int J1_ = R; int I1_ = Q; int B_ = 0; if (A >= 1 && 0 >= T) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f81; } } goto end; } loc_f703: { if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f717; } } if (nondet_bool()) { int N5_ = 14; if (0 >= B) { N5 = N5_; goto loc_f715; } } goto end; } loc_f715: { if (nondet_bool()) { int N5_ = 14; if (1 >= 0) { N5 = N5_; goto loc_f715; } } goto end; } loc_f717: { if (nondet_bool()) { int E_ = 8; if (0 >= C) { E = E_; goto loc_f727; } } goto end; } loc_f727: { if (nondet_bool()) { int M6_ = nondet(); int L_ = -1 + L; int E_ = 8; if (0 >= M6_ && 0 >= O && L >= 0) { E = E_; L = L_; M6 = M6_; goto loc_f727; } } if (nondet_bool()) { int M6_ = nondet(); int T6_ = N; int S6_ = M; int R6_ = -1 + L; int Q6_ = K; int P6_ = 10; int O6_ = D; int N6_ = J; int O_ = 1; int L_ = -1 + L; int E_ = 8; if (0 >= P && 0 >= O && M6_ >= 1 && L >= 0) { E = E_; L = L_; O = O_; M6 = M6_; N6 = N6_; O6 = O6_; P6 = P6_; Q6 = Q6_; R6 = R6_; S6 = S6_; T6 = T6_; goto loc_f727; } } if (nondet_bool()) { int K_ = 1; int E_ = 11; if (0 >= 1 + L && 0 >= A) { E = E_; K = K_; goto loc_f913; } } if (nondet_bool()) { int C7_ = 0; int B7_ = 0; int A7_ = N; int Z6_ = M; int Y6_ = L; int X6_ = 1; int W6_ = 11; int V6_ = D; int U6_ = J; int K_ = 1; int E_ = 11; if (0 >= 1 + L && A >= 1) { E = E_; K = K_; U6 = U6_; V6 = V6_; W6 = W6_; X6 = X6_; Y6 = Y6_; Z6 = Z6_; A7 = A7_; B7 = B7_; C7 = C7_; goto loc_f888; } } if (nondet_bool()) { int V7_ = 0; int U7_ = 0; int L_ = -1 + L; int E_ = 10; if (H >= 1 && O >= 1 && L >= 0) { E = E_; L = L_; U7 = U7_; V7 = V7_; goto loc_f666666; } } goto end; } loc_f758: { if (nondet_bool()) { int V6_ = nondet(); int W6_ = 2; if (1 >= 0) { V6 = V6_; W6 = W6_; goto loc_f763; } } goto end; } loc_f763: { if (nondet_bool()) { int W6_ = 3; if (0 >= A && 0 >= 1 + Z6) { W6 = W6_; goto loc_f854; } } if (nondet_bool()) { int Z6_ = -1 + Z6; int W6_ = 5; if (Z6 >= 0 && V6 >= 1) { W6 = W6_; Z6 = Z6_; goto loc_f790; } } if (nondet_bool()) { int X6_ = 0; int W6_ = 6; if (Z6 >= 0 && 0 >= V6 && 0 >= A) { W6 = W6_; X6 = X6_; goto loc_f783; } } if (nondet_bool()) { int X6_ = 0; int W6_ = 6; int G1_ = 0; int F1_ = A7; int E1_ = Z6; int D1_ = Y6; int C1_ = 0; int B1_ = 6; int A1_ = V6; int Z_ = U6; int B_ = 0; if (Z6 >= 0 && 0 >= V6 && A >= 1) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; W6 = W6_; X6 = X6_; goto loc_f783; } } if (nondet_bool()) { int W6_ = 3; int N2_ = 1; int M2_ = A7; int L2_ = Z6; int K2_ = Y6; int J2_ = X6; int I2_ = 3; int H2_ = V6; int G2_ = U6; int B_ = 1; if (0 >= 1 + Z6 && X6 >= 1 && A >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; W6 = W6_; goto loc_f854; } } if (nondet_bool()) { int W6_ = 3; int N2_ = 0; int M2_ = A7; int L2_ = Z6; int K2_ = Y6; int J2_ = X6; int I2_ = 3; int H2_ = V6; int G2_ = U6; int B_ = 0; if (0 >= 1 + Z6 && 0 >= X6 && A >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; W6 = W6_; goto loc_f854; } } goto end; } loc_f783: { if (nondet_bool()) { if (0 >= B) { goto loc_f790; } } if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f913; } } goto end; } loc_f790: { if (nondet_bool()) { if (0 >= A) { goto loc_f801; } } if (nondet_bool()) { int P1_ = 1; int O1_ = A7; int N1_ = Z6; int M1_ = Y6; int L1_ = X6; int K1_ = W6; int J1_ = V6; int I1_ = U6; int B_ = 1; if (A >= 1 && X6 >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f801; } } if (nondet_bool()) { int P1_ = 0; int O1_ = A7; int N1_ = Z6; int M1_ = Y6; int L1_ = X6; int K1_ = W6; int J1_ = V6; int I1_ = U6; int B_ = 0; if (A >= 1 && 0 >= X6) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f801; } } goto end; } loc_f801: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f819; } } if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f913; } } if (nondet_bool()) { int X1_ = 1; int W1_ = A7; int V1_ = Z6; int U1_ = Y6; int T1_ = X6; int S1_ = W6; int R1_ = V6; int Q1_ = U6; int B_ = 1; if (A >= 1 && X6 >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f819; } } if (nondet_bool()) { int X1_ = 0; int W1_ = A7; int V1_ = Z6; int U1_ = Y6; int T1_ = X6; int S1_ = W6; int R1_ = V6; int Q1_ = U6; int B_ = 0; if (A >= 1 && 0 >= X6 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f819; } } goto end; } loc_f81: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f99; } } if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f193; } } if (nondet_bool()) { int X1_ = 1; int W1_ = W; int V1_ = V; int U1_ = U; int T1_ = T; int S1_ = S; int R1_ = R; int Q1_ = Q; int B_ = 1; if (A >= 1 && T >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f99; } } if (nondet_bool()) { int X1_ = 0; int W1_ = W; int V1_ = V; int U1_ = U; int T1_ = T; int S1_ = S; int R1_ = R; int Q1_ = Q; int B_ = 0; if (A >= 1 && 0 >= T && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f99; } } goto end; } loc_f819: { if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f913; } } if (nondet_bool()) { int D7_ = 0; int C_ = 0; if (H >= 1 && C7 >= 1 && 0 >= B) { C = C_; D7 = D7_; goto loc_f913; } } if (nondet_bool()) { int E7_ = nondet(); int V6_ = nondet(); int W6_ = 2; if (0 >= E7_ && 0 >= C7 && 0 >= B) { V6 = V6_; W6 = W6_; E7 = E7_; goto loc_f763; } } if (nondet_bool()) { int E7_ = nondet(); int V6_ = nondet(); int L7_ = A7; int K7_ = Z6; int J7_ = Y6; int I7_ = X6; int H7_ = W6; int G7_ = V6; int F7_ = U6; int C7_ = 1; int W6_ = 2; if (0 >= C7 && 0 >= B7 && E7_ >= 1 && 0 >= B) { V6 = V6_; W6 = W6_; C7 = C7_; E7 = E7_; F7 = F7_; G7 = G7_; H7 = H7_; I7 = I7_; J7 = J7_; K7 = K7_; L7 = L7_; goto loc_f763; } } goto end; } loc_f854: { if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f913; } } if (nondet_bool()) { int W6_ = 8; if (0 >= B) { W6 = W6_; goto loc_f864; } } goto end; } loc_f864: { if (nondet_bool()) { int X6_ = 1; int W6_ = 11; if (0 >= 1 + Y6) { W6 = W6_; X6 = X6_; goto loc_f888; } } if (nondet_bool()) { int D7_ = 0; int Y6_ = -1 + Y6; int W6_ = 10; int C_ = 0; if (B7 >= 1 && Y6 >= 0 && H >= 1) { C = C_; W6 = W6_; Y6 = Y6_; D7 = D7_; goto loc_f913; } } if (nondet_bool()) { int M7_ = nondet(); int Y6_ = -1 + Y6; int W6_ = 8; if (0 >= B7 && Y6 >= 0 && 0 >= M7_) { W6 = W6_; Y6 = Y6_; M7 = M7_; goto loc_f864; } } if (nondet_bool()) { int M7_ = nondet(); int T7_ = A7; int S7_ = Z6; int R7_ = -1 + Y6; int Q7_ = X6; int P7_ = 10; int O7_ = V6; int N7_ = U6; int B7_ = 1; int Y6_ = -1 + Y6; int W6_ = 8; if (0 >= B7 && Y6 >= 0 && 0 >= C7 && M7_ >= 1) { W6 = W6_; Y6 = Y6_; B7 = B7_; M7 = M7_; N7 = N7_; O7 = O7_; P7 = P7_; Q7 = Q7_; R7 = R7_; S7 = S7_; T7 = T7_; goto loc_f864; } } goto end; } loc_f888: { if (nondet_bool()) { if (0 >= A) { goto loc_f899; } } if (nondet_bool()) { int D3_ = 1; int C3_ = A7; int B3_ = Z6; int A3_ = Y6; int Z2_ = X6; int Y2_ = W6; int X2_ = V6; int W2_ = U6; int B_ = 1; if (A >= 1 && X6 >= 1) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; goto loc_f899; } } if (nondet_bool()) { int D3_ = 0; int C3_ = A7; int B3_ = Z6; int A3_ = Y6; int Z2_ = X6; int Y2_ = W6; int X2_ = V6; int W2_ = U6; int B_ = 0; if (A >= 1 && 0 >= X6) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; goto loc_f899; } } goto end; } loc_f899: { if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f913; } } if (nondet_bool()) { int W6_ = 14; if (0 >= B) { W6 = W6_; goto loc_f911; } } goto end; } loc_f911: { if (nondet_bool()) { int W6_ = 14; if (1 >= 0) { W6 = W6_; goto loc_f911; } } goto end; } loc_f913: { if (nondet_bool()) { int E_ = 14; if (0 >= C) { E = E_; goto loc_f925; } } goto end; } loc_f925: { if (nondet_bool()) { int E_ = 14; if (1 >= 0) { E = E_; goto loc_f925; } } goto end; } loc_f99: { if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f193; } } if (nondet_bool()) { int H1_ = 0; int C_ = 0; if (H >= 1 && Y >= 1 && 0 >= B) { C = C_; H1 = H1_; goto loc_f193; } } if (nondet_bool()) { int Y1_ = nondet(); int R_ = nondet(); int S_ = 2; if (0 >= Y && 0 >= Y1_ && 0 >= B) { R = R_; S = S_; Y1 = Y1_; goto loc_f43; } } if (nondet_bool()) { int Y1_ = nondet(); int R_ = nondet(); int F2_ = W; int E2_ = V; int D2_ = U; int C2_ = T; int B2_ = S; int A2_ = R; int Z1_ = Q; int Y_ = 1; int S_ = 2; if (0 >= X && Y1_ >= 1 && 0 >= Y && 0 >= B) { R = R_; S = S_; Y = Y_; Y1 = Y1_; Z1 = Z1_; A2 = A2_; B2 = B2_; C2 = C2_; D2 = D2_; E2 = E2_; F2 = F2_; goto loc_f43; } } goto end; } loc_f666666: end: return 0; }