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_f105: { if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f203; } } if (nondet_bool()) { int H1_ = 0; int C_ = 0; if (H >= 1 && Y >= 1 && 0 >= B) { C = C_; H1 = H1_; goto loc_f203; } } 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 >= Y && Y1_ >= 1 && 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_f142: { if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f203; } } if (nondet_bool()) { int S_ = 8; if (0 >= B) { S = S_; goto loc_f152; } } goto end; } loc_f152: { 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_f203; } } 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_f152; } } 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) { S = S_; U = U_; X = X_; O2 = O2_; P2 = P2_; Q2 = Q2_; R2 = R2_; S2 = S2_; T2 = T2_; U2 = U2_; V2 = V2_; goto loc_f152; } } if (nondet_bool()) { int T_ = 1; int S_ = 11; if (0 >= A && 0 >= 1 + U) { S = S_; T = T_; goto loc_f189; } } 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 && H >= 1) { B = B_; S = S_; T = T_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; goto loc_f189; } } 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_f189: { if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f203; } } if (nondet_bool()) { int S_ = 14; if (0 >= B) { S = S_; goto loc_f201; } } goto end; } loc_f201: { if (nondet_bool()) { int S_ = 14; if (1 >= 0) { S = S_; goto loc_f201; } } goto end; } loc_f203: { if (nondet_bool()) { if (0 >= C) { goto loc_f210; } } goto end; } loc_f210: { if (nondet_bool()) { if (0 >= A) { goto loc_f382; } } 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_f226; } } goto end; } loc_f217: { if (nondet_bool()) { int F3_ = nondet(); int G3_ = 2; if (1 >= 0) { F3 = F3_; G3 = G3_; goto loc_f222; } } goto end; } loc_f22: { if (nondet_bool()) { int E_ = 3; if (0 >= A && 0 >= 1 + M) { E = E_; goto loc_f757; } } if (nondet_bool()) { int M_ = -1 + M; int E_ = 5; if (D >= 1 && M >= 0) { E = E_; M = M_; goto loc_f210; } } if (nondet_bool()) { int K_ = 0; int E_ = 6; if (0 >= A && M >= 0 && 0 >= D) { E = E_; K = K_; goto loc_f203; } } 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_f597; } } goto end; } loc_f222: { if (nondet_bool()) { int G3_ = 4; if (J3 >= 0) { G3 = G3_; goto loc_f226; } } if (nondet_bool()) { int G3_ = 3; if (0 >= 1 + J3 && 0 >= A) { G3 = G3_; goto loc_f321; } } 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 (H >= 1 && A >= 1 && H3 >= 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_f321; } } 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 (H >= 1 && A >= 1 && 0 >= H3 && 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_f321; } } goto end; } loc_f226: { if (nondet_bool()) { int J3_ = -1 + J3; int G3_ = 5; if (F3 >= 1) { G3 = G3_; J3 = J3_; goto loc_f251; } } if (nondet_bool()) { int H3_ = 0; int G3_ = 6; if (0 >= F3 && 0 >= A) { G3 = G3_; H3 = H3_; goto loc_f244; } } 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 (H >= 1 && A >= 1 && 0 >= F3) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; G3 = G3_; H3 = H3_; goto loc_f244; } } goto end; } loc_f244: { if (nondet_bool()) { if (0 >= B) { goto loc_f251; } } if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f382; } } goto end; } loc_f251: { if (nondet_bool()) { if (0 >= A) { goto loc_f264; } } 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 (H >= 1 && A >= 1 && H3 >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f264; } } 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 (H >= 1 && A >= 1 && 0 >= H3) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f264; } } goto end; } loc_f264: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f284; } } if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f382; } } 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 (H >= 1 && A >= 1 && 0 >= B && H3 >= 1) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f284; } } 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 (H >= 1 && A >= 1 && 0 >= B && 0 >= H3) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f284; } } goto end; } loc_f284: { if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f382; } } if (nondet_bool()) { int N3_ = 0; int C_ = 0; if (0 >= B && H >= 1 && M3 >= 1) { C = C_; N3 = N3_; goto loc_f382; } } 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_f222; } } 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 >= 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_f222; } } 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_f321: { if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f382; } } if (nondet_bool()) { int G3_ = 8; if (0 >= B) { G3 = G3_; goto loc_f331; } } goto end; } loc_f331: { 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_f382; } } 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_f331; } } 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) { G3 = G3_; I3 = I3_; L3 = L3_; W3 = W3_; X3 = X3_; Y3 = Y3_; Z3 = Z3_; A4 = A4_; B4 = B4_; C4 = C4_; D4 = D4_; goto loc_f331; } } if (nondet_bool()) { int H3_ = 1; int G3_ = 11; if (0 >= 1 + I3 && 0 >= A) { G3 = G3_; H3 = H3_; goto loc_f368; } } 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 (H >= 1 && A >= 1 && 0 >= 1 + I3) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; G3 = G3_; H3 = H3_; goto loc_f368; } } goto end; } loc_f368: { if (nondet_bool()) { int N3_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N3 = N3_; goto loc_f382; } } if (nondet_bool()) { int G3_ = 14; if (0 >= B) { G3 = G3_; goto loc_f380; } } 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_f380: { if (nondet_bool()) { int G3_ = 14; if (1 >= 0) { G3 = G3_; goto loc_f380; } } goto end; } loc_f382: { if (nondet_bool()) { if (0 >= C && 0 >= A) { goto loc_f561; } } 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_f401; } } goto end; } loc_f396: { if (nondet_bool()) { int F4_ = nondet(); int G4_ = 2; if (1 >= 0) { F4 = F4_; G4 = G4_; goto loc_f401; } } goto end; } loc_f401: { if (nondet_bool()) { int G4_ = 3; if (0 >= A && 0 >= 1 + J4) { G4 = G4_; goto loc_f500; } } if (nondet_bool()) { int J4_ = -1 + J4; int G4_ = 5; if (J4 >= 0 && F4 >= 1) { G4 = G4_; J4 = J4_; goto loc_f430; } } if (nondet_bool()) { int H4_ = 0; int G4_ = 6; if (J4 >= 0 && 0 >= F4 && 0 >= A) { G4 = G4_; H4 = H4_; goto loc_f423; } } 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 && H >= 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_f423; } } 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 && H >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; G4 = G4_; goto loc_f500; } } 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 && H >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; G4 = G4_; goto loc_f500; } } goto end; } loc_f423: { if (nondet_bool()) { if (0 >= B) { goto loc_f430; } } if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f561; } } goto end; } loc_f43: { if (nondet_bool()) { int S_ = 3; if (0 >= A && 0 >= 1 + V) { S = S_; goto loc_f142; } } 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_f72; } } 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 && H >= 1) { B = B_; S = S_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; goto loc_f142; } } 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 && H >= 1) { B = B_; S = S_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; goto loc_f142; } } goto end; } loc_f430: { if (nondet_bool()) { if (0 >= A) { goto loc_f443; } } 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 && H >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f443; } } 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 && H >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f443; } } goto end; } loc_f443: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f463; } } if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f561; } } 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 && H >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f463; } } 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 && H >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f463; } } goto end; } loc_f463: { if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f561; } } if (nondet_bool()) { int N4_ = 0; int C_ = 0; if (H >= 1 && M4 >= 1 && 0 >= B) { C = C_; N4 = N4_; goto loc_f561; } } 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_f401; } } 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 (O4_ >= 1 && 0 >= M4 && 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_f401; } } goto end; } loc_f500: { if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f561; } } if (nondet_bool()) { int G4_ = 8; if (0 >= B) { G4 = G4_; goto loc_f510; } } goto end; } loc_f510: { 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_f561; } } 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_f510; } } 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 && 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_f510; } } if (nondet_bool()) { int H4_ = 1; int G4_ = 11; if (0 >= A && 0 >= 1 + I4) { G4 = G4_; H4 = H4_; goto loc_f547; } } 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 && H >= 1) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; G4 = G4_; H4 = H4_; goto loc_f547; } } goto end; } loc_f52: { if (nondet_bool()) { if (0 >= A) { goto loc_f65; } } 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 && H >= 1) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f65; } } 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 && H >= 1) { B = B_; Z = Z_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f65; } } goto end; } loc_f547: { if (nondet_bool()) { int N4_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; N4 = N4_; goto loc_f561; } } if (nondet_bool()) { int G4_ = 14; if (0 >= B) { G4 = G4_; goto loc_f559; } } goto end; } loc_f559: { if (nondet_bool()) { int G4_ = 14; if (1 >= 0) { G4 = G4_; goto loc_f559; } } goto end; } loc_f561: { 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 (E5_ >= 1 && 0 >= P && 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_f592: { if (nondet_bool()) { int M5_ = nondet(); int N5_ = 2; if (1 >= 0) { M5 = M5_; N5 = N5_; goto loc_f597; } } goto end; } loc_f597: { if (nondet_bool()) { int N5_ = 3; if (0 >= A && 0 >= 1 + R5) { N5 = N5_; goto loc_f696; } } if (nondet_bool()) { int R5_ = -1 + R5; int N5_ = 5; if (R5 >= 0 && M5 >= 1) { N5 = N5_; R5 = R5_; goto loc_f626; } } if (nondet_bool()) { int P5_ = 0; int N5_ = 6; if (R5 >= 0 && 0 >= M5 && 0 >= A) { N5 = N5_; P5 = P5_; goto loc_f619; } } 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 && H >= 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_f619; } } 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 && H >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; N5 = N5_; goto loc_f696; } } 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 && H >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; N5 = N5_; goto loc_f696; } } goto end; } loc_f619: { if (nondet_bool()) { if (0 >= B) { goto loc_f626; } } if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f757; } } goto end; } loc_f626: { if (nondet_bool()) { if (0 >= A) { goto loc_f639; } } 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 && H >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f639; } } 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 && H >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f639; } } goto end; } loc_f639: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f659; } } if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f757; } } 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 && H >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f659; } } 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 && H >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f659; } } goto end; } loc_f65: { if (nondet_bool()) { if (0 >= B) { goto loc_f72; } } if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f203; } } goto end; } loc_f659: { if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f757; } } if (nondet_bool()) { int V5_ = 0; int C_ = 0; if (H >= 1 && U5 >= 1 && 0 >= B) { C = C_; V5 = V5_; goto loc_f757; } } 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_f597; } } 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 (W5_ >= 1 && 0 >= U5 && 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_f597; } } goto end; } loc_f696: { if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f757; } } if (nondet_bool()) { int N5_ = 8; if (0 >= B) { N5 = N5_; goto loc_f706; } } goto end; } loc_f706: { 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_f757; } } 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_f706; } } 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 && 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_f706; } } if (nondet_bool()) { int P5_ = 1; int N5_ = 11; if (0 >= A && 0 >= 1 + Q5) { N5 = N5_; P5 = P5_; goto loc_f743; } } 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 && H >= 1) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; N5 = N5_; P5 = P5_; goto loc_f743; } } goto end; } loc_f72: { if (nondet_bool()) { if (0 >= A) { goto loc_f85; } } 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 && H >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f85; } } 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 && H >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f85; } } goto end; } loc_f743: { if (nondet_bool()) { int V5_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; V5 = V5_; goto loc_f757; } } if (nondet_bool()) { int N5_ = 14; if (0 >= B) { N5 = N5_; goto loc_f755; } } goto end; } loc_f755: { if (nondet_bool()) { int N5_ = 14; if (1 >= 0) { N5 = N5_; goto loc_f755; } } goto end; } loc_f757: { if (nondet_bool()) { int E_ = 8; if (0 >= C) { E = E_; goto loc_f767; } } goto end; } loc_f767: { 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_f767; } } 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 (M6_ >= 1 && 0 >= O && 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_f767; } } if (nondet_bool()) { int K_ = 1; int E_ = 11; if (0 >= 1 + L && 0 >= A) { E = E_; K = K_; goto loc_f963; } } 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_f936; } } 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_f798: { if (nondet_bool()) { int V6_ = nondet(); int W6_ = 2; if (1 >= 0) { V6 = V6_; W6 = W6_; goto loc_f803; } } goto end; } loc_f803: { if (nondet_bool()) { int W6_ = 3; if (0 >= A && 0 >= 1 + Z6) { W6 = W6_; goto loc_f902; } } if (nondet_bool()) { int Z6_ = -1 + Z6; int W6_ = 5; if (Z6 >= 0 && V6 >= 1) { W6 = W6_; Z6 = Z6_; goto loc_f832; } } if (nondet_bool()) { int X6_ = 0; int W6_ = 6; if (Z6 >= 0 && 0 >= V6 && 0 >= A) { W6 = W6_; X6 = X6_; goto loc_f825; } } 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 && H >= 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_f825; } } 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 && H >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; W6 = W6_; goto loc_f902; } } 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 && H >= 1) { B = B_; G2 = G2_; H2 = H2_; I2 = I2_; J2 = J2_; K2 = K2_; L2 = L2_; M2 = M2_; N2 = N2_; W6 = W6_; goto loc_f902; } } goto end; } loc_f825: { if (nondet_bool()) { if (0 >= B) { goto loc_f832; } } if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f963; } } goto end; } loc_f832: { if (nondet_bool()) { if (0 >= A) { goto loc_f845; } } 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 && H >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f845; } } 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 && H >= 1) { B = B_; I1 = I1_; J1 = J1_; K1 = K1_; L1 = L1_; M1 = M1_; N1 = N1_; O1 = O1_; P1 = P1_; goto loc_f845; } } goto end; } loc_f845: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f865; } } if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f963; } } 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 && H >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f865; } } 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 && H >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f865; } } goto end; } loc_f85: { if (nondet_bool()) { if (0 >= B && 0 >= A) { goto loc_f105; } } if (nondet_bool()) { int H1_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; H1 = H1_; goto loc_f203; } } 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 && H >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f105; } } 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 && H >= 1 && 0 >= B) { B = B_; Q1 = Q1_; R1 = R1_; S1 = S1_; T1 = T1_; U1 = U1_; V1 = V1_; W1 = W1_; X1 = X1_; goto loc_f105; } } goto end; } loc_f865: { if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f963; } } if (nondet_bool()) { int D7_ = 0; int C_ = 0; if (H >= 1 && C7 >= 1 && 0 >= B) { C = C_; D7 = D7_; goto loc_f963; } } 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_f803; } } 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 (E7_ >= 1 && 0 >= C7 && 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_f803; } } goto end; } loc_f902: { if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f963; } } if (nondet_bool()) { int W6_ = 8; if (0 >= B) { W6 = W6_; goto loc_f912; } } goto end; } loc_f912: { if (nondet_bool()) { int X6_ = 1; int W6_ = 11; if (0 >= 1 + Y6) { W6 = W6_; X6 = X6_; goto loc_f936; } } 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_f963; } } 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_f912; } } 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 && 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_f912; } } goto end; } loc_f936: { if (nondet_bool()) { if (0 >= A) { goto loc_f949; } } 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 && H >= 1) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; goto loc_f949; } } 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 && H >= 1) { B = B_; W2 = W2_; X2 = X2_; Y2 = Y2_; Z2 = Z2_; A3 = A3_; B3 = B3_; C3 = C3_; D3 = D3_; goto loc_f949; } } goto end; } loc_f949: { if (nondet_bool()) { int D7_ = 1; int C_ = 1; if (B >= 1 && H >= 1) { C = C_; D7 = D7_; goto loc_f963; } } if (nondet_bool()) { int W6_ = 14; if (0 >= B) { W6 = W6_; goto loc_f961; } } goto end; } loc_f961: { if (nondet_bool()) { int W6_ = 14; if (1 >= 0) { W6 = W6_; goto loc_f961; } } goto end; } loc_f963: { if (nondet_bool()) { int E_ = 14; if (0 >= C) { E = E_; goto loc_f975; } } goto end; } loc_f975: { if (nondet_bool()) { int E_ = 14; if (1 >= 0) { E = E_; goto loc_f975; } } goto end; } loc_f666666: end: return 0; }