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) { goto loc_f9; loc_f1: { if (nondet_bool()) { int U_ = nondet(); int S_ = nondet(); int V_ = A; int T_ = S; int R_ = S; int A_ = 1 + A; if (A >= 0 && Q >= 1 + A) { A = A_; R = R_; S = S_; T = T_; U = U_; V = V_; goto loc_f1; } } if (nondet_bool()) { int Z_ = nondet(); int Y_ = nondet(); int X_ = nondet(); int W_ = nondet(); int T_ = nondet(); int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int D_ = nondet(); int E_ = R; int C_ = 0; int B_ = R; int A_ = H; if (C == 0 && H >= D_ && Z_ >= D_ && 0 >= 1 + R && D_ >= 2 && A >= 0 && A >= Q) { A = A_; B = B_; C = C_; D = D_; E = E_; Q = Q_; R = R_; S = S_; T = T_; W = W_; X = X_; Y = Y_; Z = Z_; goto loc_f16; } } if (nondet_bool()) { int Z_ = nondet(); int Y_ = nondet(); int X_ = nondet(); int W_ = nondet(); int T_ = nondet(); int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int D_ = nondet(); int E_ = R; int C_ = 0; int B_ = R; int A_ = H; if (C == 0 && H >= D_ && Z_ >= D_ && R >= 1 && D_ >= 2 && A >= 0 && A >= Q) { A = A_; B = B_; C = C_; D = D_; E = E_; Q = Q_; R = R_; S = S_; T = T_; W = W_; X = X_; Y = Y_; Z = Z_; goto loc_f16; } } goto end; } loc_f12: { if (nondet_bool()) { int Y_0 = nondet(); int I_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int J_ = H; int G_ = 1 + H; int C_ = 1; if (C == 1 && 0 >= 1 + E_ && Y_0 >= D_ && 0 >= 1 + B && D_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; G = G_; I = I_; J = J_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int I_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int J_ = H; int G_ = 1 + H; int C_ = 1; if (C == 1 && E_ >= 1 && Y_0 >= D_ && 0 >= 1 + B && D_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; G = G_; I = I_; J = J_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int I_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int J_ = H; int G_ = 1 + H; int C_ = 1; if (C == 1 && 0 >= 1 + E_ && Y_0 >= D_ && B >= 1 && D_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; G = G_; I = I_; J = J_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int I_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int J_ = H; int G_ = 1 + H; int C_ = 1; if (C == 1 && E_ >= 1 && Y_0 >= D_ && B >= 1 && D_ >= 2 && A >= 0) { C = C_; D = D_; E = E_; F = F_; G = G_; I = I_; J = J_; goto loc_f16; } } goto end; } loc_f13: { if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (0 >= 1 + L_ && 0 >= 1 + E_ && 0 >= 1 + B && D_ >= 2 && J >= 0) { D = D_; E = E_; K = K_; L = L_; goto loc_f16; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (L_ >= 1 && 0 >= 1 + E_ && 0 >= 1 + B && D_ >= 2 && J >= 0) { D = D_; E = E_; K = K_; L = L_; goto loc_f16; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (0 >= 1 + L_ && E_ >= 1 && 0 >= 1 + B && D_ >= 2 && J >= 0) { D = D_; E = E_; K = K_; L = L_; goto loc_f16; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (L_ >= 1 && E_ >= 1 && 0 >= 1 + B && D_ >= 2 && J >= 0) { D = D_; E = E_; K = K_; L = L_; goto loc_f16; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (0 >= 1 + L_ && 0 >= 1 + E_ && B >= 1 && D_ >= 2 && J >= 0) { D = D_; E = E_; K = K_; L = L_; goto loc_f16; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (L_ >= 1 && 0 >= 1 + E_ && B >= 1 && D_ >= 2 && J >= 0) { D = D_; E = E_; K = K_; L = L_; goto loc_f16; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (0 >= 1 + L_ && E_ >= 1 && B >= 1 && D_ >= 2 && J >= 0) { D = D_; E = E_; K = K_; L = L_; goto loc_f16; } } if (nondet_bool()) { int L_ = nondet(); int K_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (L_ >= 1 && E_ >= 1 && B >= 1 && D_ >= 2 && J >= 0) { D = D_; E = E_; K = K_; L = L_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int G1_ = E; int F1_ = E; int E1_ = 0; int D1_ = E; int C1_ = 0; int B1_ = H1; int A1_ = E; int J_ = 0; int C_ = 1 + H1; int B_ = 0; if (C == 1 && J == 0 && B == 0 && 0 >= 1 + E && D_ >= 2 && E >= 1 && Y_0 >= 2) { B = B_; C = C_; D = D_; J = J_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int G1_ = E; int F1_ = E; int E1_ = 0; int D1_ = E; int C1_ = 0; int B1_ = H1; int A1_ = E; int J_ = 0; int C_ = 1 + H1; int B_ = 0; if (C == 1 && J == 0 && B == 0 && D_ >= 2 && E >= 1 && Y_0 >= 2) { B = B_; C = C_; D = D_; J = J_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int G1_ = E; int F1_ = E; int E1_ = 0; int D1_ = E; int C1_ = 0; int B1_ = H1; int A1_ = E; int J_ = 0; int C_ = 1 + H1; int B_ = 0; if (C == 1 && J == 0 && B == 0 && D_ >= 2 && 0 >= 1 + E && Y_0 >= 2) { B = B_; C = C_; D = D_; J = J_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int G1_ = E; int F1_ = E; int E1_ = 0; int D1_ = E; int C1_ = 0; int B1_ = H1; int A1_ = E; int J_ = 0; int C_ = 1 + H1; int B_ = 0; if (C == 1 && J == 0 && B == 0 && E >= 1 && D_ >= 2 && 0 >= 1 + E && Y_0 >= 2) { B = B_; C = C_; D = D_; J = J_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } goto end; } loc_f16: { if (nondet_bool()) { int Y_0 = nondet(); int N_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int P_ = -1 + H; int O_ = 1 + C; int M_ = B; int H_ = -1 + H; int C_ = 1 + C; if (0 >= 1 + N_ && 0 >= 1 + E_ && 0 >= 1 + Y_0 && D_ >= 2 && H >= 0 && C >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; M = M_; N = N_; O = O_; P = P_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int N_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int P_ = -1 + H; int O_ = 1 + C; int M_ = B; int H_ = -1 + H; int C_ = 1 + C; if (N_ >= 1 && 0 >= 1 + E_ && 0 >= 1 + Y_0 && D_ >= 2 && H >= 0 && C >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; M = M_; N = N_; O = O_; P = P_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int N_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int P_ = -1 + H; int O_ = 1 + C; int M_ = B; int H_ = -1 + H; int C_ = 1 + C; if (0 >= 1 + N_ && E_ >= 1 && 0 >= 1 + Y_0 && D_ >= 2 && H >= 0 && C >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; M = M_; N = N_; O = O_; P = P_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int N_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int P_ = -1 + H; int O_ = 1 + C; int M_ = B; int H_ = -1 + H; int C_ = 1 + C; if (N_ >= 1 && E_ >= 1 && 0 >= 1 + Y_0 && D_ >= 2 && H >= 0 && C >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; M = M_; N = N_; O = O_; P = P_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int N_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int P_ = -1 + H; int O_ = 1 + C; int M_ = B; int H_ = -1 + H; int C_ = 1 + C; if (0 >= 1 + N_ && 0 >= 1 + E_ && Y_0 >= 1 && D_ >= 2 && H >= 0 && C >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; M = M_; N = N_; O = O_; P = P_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int N_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int P_ = -1 + H; int O_ = 1 + C; int M_ = B; int H_ = -1 + H; int C_ = 1 + C; if (N_ >= 1 && 0 >= 1 + E_ && Y_0 >= 1 && D_ >= 2 && H >= 0 && C >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; M = M_; N = N_; O = O_; P = P_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int N_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int P_ = -1 + H; int O_ = 1 + C; int M_ = B; int H_ = -1 + H; int C_ = 1 + C; if (0 >= 1 + N_ && E_ >= 1 && Y_0 >= 1 && D_ >= 2 && H >= 0 && C >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; M = M_; N = N_; O = O_; P = P_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int N_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int P_ = -1 + H; int O_ = 1 + C; int M_ = B; int H_ = -1 + H; int C_ = 1 + C; if (N_ >= 1 && E_ >= 1 && Y_0 >= 1 && D_ >= 2 && H >= 0 && C >= 0) { C = C_; D = D_; E = E_; F = F_; H = H_; M = M_; N = N_; O = O_; P = P_; goto loc_f16; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int G1_ = E; int F1_ = E; int E1_ = 0; int D1_ = E; int C1_ = 0; int B1_ = H1; int A1_ = E; int C_ = 1 + H1; int B_ = 0; if (B == 0 && 0 >= 1 + E && H >= 0 && C >= 0 && D_ >= 2 && E >= 1 && Y_0 >= 2) { B = B_; C = C_; D = D_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int G1_ = E; int F1_ = E; int E1_ = 0; int D1_ = E; int C1_ = 0; int B1_ = H1; int A1_ = E; int C_ = 1 + H1; int B_ = 0; if (B == 0 && H >= 0 && C >= 0 && D_ >= 2 && E >= 1 && Y_0 >= 2) { B = B_; C = C_; D = D_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int G1_ = E; int F1_ = E; int E1_ = 0; int D1_ = E; int C1_ = 0; int B1_ = H1; int A1_ = E; int C_ = 1 + H1; int B_ = 0; if (B == 0 && H >= 0 && C >= 0 && D_ >= 2 && 0 >= 1 + E && Y_0 >= 2) { B = B_; C = C_; D = D_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int D_ = nondet(); int G1_ = E; int F1_ = E; int E1_ = 0; int D1_ = E; int C1_ = 0; int B1_ = H1; int A1_ = E; int C_ = 1 + H1; int B_ = 0; if (B == 0 && E >= 1 && H >= 0 && C >= 0 && D_ >= 2 && 0 >= 1 + E && Y_0 >= 2) { B = B_; C = C_; D = D_; A1 = A1_; B1 = B1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } goto end; } loc_f7: { if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && 0 >= 1 + F1_ && F1_ >= 1 + Y_0 && D_ >= 2 && B1 >= 0 && Y_0 >= 1 + A1) { B = B_; D = D_; E = E_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && F1_ >= 1 && F1_ >= 1 + Y_0 && D_ >= 2 && B1 >= 0 && Y_0 >= 1 + A1) { B = B_; D = D_; E = E_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && 0 >= 1 + F1_ && Y_0 >= 1 + F1_ && D_ >= 2 && B1 >= 0 && Y_0 >= 1 + A1) { B = B_; D = D_; E = E_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && F1_ >= 1 && Y_0 >= 1 + F1_ && D_ >= 2 && B1 >= 0 && Y_0 >= 1 + A1) { B = B_; D = D_; E = E_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && 0 >= 1 + F1_ && F1_ >= 1 + Y_0 && D_ >= 2 && B1 >= 0 && A1 >= 1 + Y_0) { B = B_; D = D_; E = E_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && F1_ >= 1 && F1_ >= 1 + Y_0 && D_ >= 2 && B1 >= 0 && A1 >= 1 + Y_0) { B = B_; D = D_; E = E_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && 0 >= 1 + F1_ && Y_0 >= 1 + F1_ && D_ >= 2 && B1 >= 0 && A1 >= 1 + Y_0) { B = B_; D = D_; E = E_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int E_ = nondet(); int D_ = nondet(); int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && F1_ >= 1 && Y_0 >= 1 + F1_ && D_ >= 2 && B1 >= 0 && A1 >= 1 + Y_0) { B = B_; D = D_; E = E_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f8; } } if (nondet_bool()) { int G1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int A1_ = nondet(); int Y_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (C1 == A1 && D_ >= 2 && 0 >= 1 + E_ && B1 >= 0) { D = D_; E = E_; Y = Y_; A1 = A1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f10; } } if (nondet_bool()) { int G1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int A1_ = nondet(); int Y_ = nondet(); int E_ = nondet(); int D_ = nondet(); if (C1 == A1 && D_ >= 2 && E_ >= 1 && B1 >= 0) { D = D_; E = E_; Y = Y_; A1 = A1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f10; } } goto end; } loc_f8: { if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int I1_ = -1 + H1; int H1_ = -1 + H1; int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && 0 >= 1 + F1_ && F1_ >= 1 + Y_0 && D_ >= 2 && H1 >= 0 && Y_0 >= 1 + A1) { B = B_; D = D_; E = E_; F = F_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int I1_ = -1 + H1; int H1_ = -1 + H1; int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && F1_ >= 1 && F1_ >= 1 + Y_0 && D_ >= 2 && H1 >= 0 && Y_0 >= 1 + A1) { B = B_; D = D_; E = E_; F = F_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int I1_ = -1 + H1; int H1_ = -1 + H1; int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && 0 >= 1 + F1_ && Y_0 >= 1 + F1_ && D_ >= 2 && H1 >= 0 && Y_0 >= 1 + A1) { B = B_; D = D_; E = E_; F = F_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int I1_ = -1 + H1; int H1_ = -1 + H1; int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && F1_ >= 1 && Y_0 >= 1 + F1_ && D_ >= 2 && H1 >= 0 && Y_0 >= 1 + A1) { B = B_; D = D_; E = E_; F = F_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int I1_ = -1 + H1; int H1_ = -1 + H1; int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && 0 >= 1 + F1_ && F1_ >= 1 + Y_0 && D_ >= 2 && H1 >= 0 && A1 >= 1 + Y_0) { B = B_; D = D_; E = E_; F = F_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int I1_ = -1 + H1; int H1_ = -1 + H1; int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && F1_ >= 1 && F1_ >= 1 + Y_0 && D_ >= 2 && H1 >= 0 && A1 >= 1 + Y_0) { B = B_; D = D_; E = E_; F = F_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int I1_ = -1 + H1; int H1_ = -1 + H1; int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && 0 >= 1 + F1_ && Y_0 >= 1 + F1_ && D_ >= 2 && H1 >= 0 && A1 >= 1 + Y_0) { B = B_; D = D_; E = E_; F = F_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f8; } } if (nondet_bool()) { int Y_0 = nondet(); int F1_ = nondet(); int D1_ = nondet(); int F_ = nondet(); int E_ = nondet(); int D_ = nondet(); int I1_ = -1 + H1; int H1_ = -1 + H1; int G1_ = A1; int E1_ = 0; int C1_ = 0; int B_ = 0; if (C1 == 0 && F1_ >= 1 && Y_0 >= 1 + F1_ && D_ >= 2 && H1 >= 0 && A1 >= 1 + Y_0) { B = B_; D = D_; E = E_; F = F_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; H1 = H1_; I1 = I1_; goto loc_f8; } } if (nondet_bool()) { int G1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int A1_ = nondet(); int Y_ = nondet(); int D_ = nondet(); if (C1 == A1 && H1 >= 0 && D_ >= 2) { D = D_; Y = Y_; A1 = A1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; goto loc_f10; } } goto end; } loc_f9: { if (nondet_bool()) { int K1_ = nondet(); int J1_ = nondet(); int W_ = nondet(); int T_ = nondet(); int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int D_ = nondet(); int A_ = 2; if (Q_ >= 2) { A = A_; D = D_; Q = Q_; R = R_; S = S_; T = T_; W = W_; J1 = J1_; K1 = K1_; goto loc_f1; } } if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int Y_2 = nondet(); int J1_ = nondet(); int G1_ = nondet(); int F1_ = nondet(); int E1_ = nondet(); int D1_ = nondet(); int C1_ = nondet(); int A1_ = nondet(); int Y_ = nondet(); int X_ = nondet(); int W_ = nondet(); int T_ = nondet(); int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int D_ = nondet(); int A_ = nondet(); int E_ = 0; int B_ = 0; if (0 >= Y_0 && 0 >= D_ && 0 >= Y_1 && 0 >= Y_2) { A = A_; B = B_; D = D_; E = E_; Q = Q_; R = R_; S = S_; T = T_; W = W_; X = X_; Y = Y_; A1 = A1_; C1 = C1_; D1 = D1_; E1 = E1_; F1 = F1_; G1 = G1_; J1 = J1_; goto loc_f10; } } goto end; } loc_f10: end: return 0; }