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) { goto loc_f2; loc_f101: { if (nondet_bool()) { int P_ = nondet(); int K_ = nondet(); int A1_ = 1 + A1; if (C >= 1 + A1) { K = K_; P = P_; A1 = A1_; goto loc_f101; } } if (nondet_bool()) { if (A1 >= C) { goto loc_f110; } } goto end; } loc_f110: { if (nondet_bool()) { int P_ = nondet(); int K_ = nondet(); int A1_ = 1 + A1; if (A >= A1) { K = K_; P = P_; A1 = A1_; goto loc_f110; } } if (nondet_bool()) { if (A1 >= 1 + A) { goto loc_f119; } } goto end; } loc_f119: { if (nondet_bool()) { int P_ = nondet(); int K_ = nondet(); int A1_ = 1 + A1; if (A >= A1) { K = K_; P = P_; A1 = A1_; goto loc_f119; } } if (nondet_bool()) { int C_ = 1 + C; if (A1 >= 1 + A) { C = C_; goto loc_f53; } } goto end; } loc_f132: { if (nondet_bool()) { int B_ = 1 + B; if (A >= B) { B = B_; goto loc_f132; } } if (nondet_bool()) { int E_ = 1 + E; if (B >= 1 + A) { E = E_; goto loc_f27; } } goto end; } loc_f17: { if (nondet_bool()) { int D_ = nondet(); int B_ = 1 + B; if (A >= B) { B = B_; D = D_; goto loc_f17; } } if (nondet_bool()) { if (B >= 1 + A) { goto loc_f27; } } goto end; } loc_f2: { if (nondet_bool()) { if (1 >= 0) { goto loc_f5; } } goto end; } loc_f27: { if (nondet_bool()) { int F_ = 0; if (50 >= E) { F = F_; goto loc_f31; } } if (nondet_bool()) { if (E >= 51) { goto loc_f1; } } goto end; } loc_f31: { if (nondet_bool()) { if (A >= 1 + B) { goto loc_f34; } } if (nondet_bool()) { if (0 >= 1 + F && B >= A) { goto loc_f46; } } if (nondet_bool()) { if (F >= 1 && B >= A) { goto loc_f46; } } if (nondet_bool()) { int F_ = 0; if (F == 0 && B >= A) { F = F_; goto loc_f1; } } goto end; } loc_f34: { if (nondet_bool()) { int G_ = nondet(); int F_ = F + G_; int C_ = 1 + C; if (A >= C) { C = C_; F = F_; G = G_; goto loc_f34; } } if (nondet_bool()) { int B_ = 1 + B; if (C >= 1 + A) { B = B_; goto loc_f31; } } goto end; } loc_f46: { if (nondet_bool()) { int H_ = nondet(); if (3 >= E) { H = H_; goto loc_f50; } } if (nondet_bool()) { int H_ = 0; if (E >= 4) { H = H_; goto loc_f50; } } goto end; } loc_f5: { if (nondet_bool()) { if (A >= B) { goto loc_f8; } } if (nondet_bool()) { if (B >= 1 + A) { goto loc_f17; } } goto end; } loc_f50: { if (nondet_bool()) { if (A >= 1 + B) { goto loc_f53; } } if (nondet_bool()) { if (B >= A) { goto loc_f132; } } goto end; } loc_f53: { if (nondet_bool()) { int N_ = nondet(); int L_ = nondet(); int J_ = nondet(); int O_ = N_ + 100 * J_; int M_ = L_ + 100 * J_; int K_ = 100 * J_; int C_ = 1 + C; if (E >= 5 && A >= C) { C = C_; J = J_; K = K_; L = L_; M = M_; N = N_; O = O_; goto loc_f53; } } if (nondet_bool()) { int J_ = nondet(); int I_ = nondet(); int K_ = 100 * J_; if (4 >= E && A >= C) { I = I_; J = J_; K = K_; goto loc_f69; } } if (nondet_bool()) { int O_ = nondet(); int N_ = nondet(); int L_ = nondet(); int J_ = nondet(); int I_ = nondet(); int M_ = L_ + 100 * J_; int K_ = 100 * J_; if (O_ >= 1 + N_ + 100 * J_ && A >= C && E >= 5) { I = I_; J = J_; K = K_; L = L_; M = M_; N = N_; O = O_; goto loc_f69; } } if (nondet_bool()) { int O_ = nondet(); int N_ = nondet(); int L_ = nondet(); int J_ = nondet(); int I_ = nondet(); int M_ = L_ + 100 * J_; int K_ = 100 * J_; if (N_ + 100 * J_ >= 1 + O_ && A >= C && E >= 5) { I = I_; J = J_; K = K_; L = L_; M = M_; N = N_; O = O_; goto loc_f69; } } if (nondet_bool()) { int M_ = nondet(); int L_ = nondet(); int J_ = nondet(); int I_ = nondet(); int K_ = 100 * J_; if (M_ >= 1 + L_ + 100 * J_ && A >= C && E >= 5) { I = I_; J = J_; K = K_; L = L_; M = M_; goto loc_f69; } } if (nondet_bool()) { int M_ = nondet(); int L_ = nondet(); int J_ = nondet(); int I_ = nondet(); int K_ = 100 * J_; if (L_ + 100 * J_ >= 1 + M_ && A >= C && E >= 5) { I = I_; J = J_; K = K_; L = L_; M = M_; goto loc_f69; } } if (nondet_bool()) { int B_ = 1 + B; if (C >= 1 + A) { B = B_; goto loc_f50; } } goto end; } loc_f69: { if (nondet_bool()) { int C_ = 1 + C; if (H >= I) { C = C_; goto loc_f53; } } if (nondet_bool()) { int Y_2 = nondet(); int Y_3 = nondet(); int Y_0 = nondet(); int Y_1 = nondet(); int V_ = nondet(); int U_ = nondet(); int T_ = nondet(); int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int P_ = Y_2 + -Y_3; if (I >= 1 + H && Y_0 >= S_ && U_ * Y_0 + V_ * Y_0 + Y_0 >= 2 && 1 >= U_ * Y_0 + V_ * Y_0 && S_ >= Y_1 && U_ * Y_1 + V_ * Y_1 + Y_1 >= 2 && 1 >= U_ * Y_1 + V_ * Y_1 && R_ >= 1 + Q_ + K) { P = P_; Q = Q_; R = R_; S = S_; T = T_; U = U_; V = V_; goto loc_f80; } } if (nondet_bool()) { int Y_2 = nondet(); int Y_3 = nondet(); int Y_0 = nondet(); int Y_1 = nondet(); int V_ = nondet(); int U_ = nondet(); int T_ = nondet(); int S_ = nondet(); int R_ = nondet(); int Q_ = nondet(); int P_ = Y_2 + -Y_3; if (I >= 1 + H && Y_0 >= S_ && U_ * Y_0 + V_ * Y_0 + Y_0 >= 2 && 1 >= U_ * Y_0 + V_ * Y_0 && S_ >= Y_1 && U_ * Y_1 + V_ * Y_1 + Y_1 >= 2 && 1 >= U_ * Y_1 + V_ * Y_1 && Q_ + K >= 1 + R_) { P = P_; Q = Q_; R = R_; S = S_; T = T_; U = U_; V = V_; goto loc_f80; } } if (nondet_bool()) { int Y_0 = nondet(); int Y_1 = nondet(); int Y_2 = nondet(); int Y_3 = nondet(); int Y_4 = nondet(); int Y_5 = nondet(); int Y_6 = nondet(); int Y_7 = nondet(); int Y_8 = nondet(); int Y_9 = nondet(); int Y_10 = nondet(); int Y_11 = nondet(); int Y_12 = nondet(); int Y_13 = nondet(); int Y_14 = nondet(); int Y_15 = nondet(); int Y_16 = nondet(); int Y_17 = nondet(); int Y_18 = nondet(); int Y_19 = nondet(); int Y_20 = nondet(); int Y_21 = nondet(); int Y_22 = nondet(); int Y_23 = nondet(); int Y_24 = nondet(); int Y_25 = nondet(); int Y_26 = nondet(); int Y_27 = nondet(); int Y_28 = nondet(); int Y_29 = nondet(); int Z_ = nondet(); int Y_ = nondet(); int X_ = nondet(); int W_ = nondet(); int S_ = nondet(); int Q_ = nondet(); int P_ = nondet(); int R_ = Q_ + K; if (I >= 1 + H && Y_0 >= X_ && W_ * Y_0 + Y_0 >= 2 && 1 >= W_ * Y_0 && X_ >= Y_1 && W_ * Y_1 + Y_1 >= 2 && 1 >= W_ * Y_1 && P_ >= Y_2 && Y_2 * Y_3 * Y_4 + Y_2 >= 1 + Y_2 * Y_3 * Y_5 + Y_3 * Y_6 && Y_3 * Y_6 + Y_2 * Y_3 * Y_5 >= Y_2 * Y_3 * Y_4 && Y_7 >= P_ && Y_3 * Y_4 * Y_7 + Y_7 >= 1 + Y_3 * Y_5 * Y_7 + Y_3 * Y_6 && Y_3 * Y_6 + Y_3 * Y_5 * Y_7 >= Y_3 * Y_4 * Y_7 && S_ >= Y_8 && Y_4 * Y_8 + Y_8 >= 1 + Y_5 * Y_8 + Y_6 && Y_6 + Y_5 * Y_8 >= Y_4 * Y_8 && Y_9 >= S_ && Y_4 * Y_9 + Y_9 >= 1 + Y_5 * Y_9 + Y_6 && Y_6 + Y_5 * Y_9 >= Y_4 * Y_9 && Z_ >= Y_10 && 2 * Y_10 + Y_10 * Y_11 >= 1 + Y_12 && Y_12 >= Y_10 + Y_10 * Y_11 && W_ * Y_11 + Y_11 >= 2 && 1 >= W_ * Y_11 && Y_12 * Y_13 + Y_12 >= 1 + Y_12 * Y_14 + Y_15 && Y_15 + Y_12 * Y_14 >= Y_12 * Y_13 && W_ * Y_14 * Y_5 + Y_14 >= 1 + Y_5 && Y_5 >= W_ * Y_14 * Y_5 && W_ * Y_13 * Y_4 + Y_13 >= 1 + Y_4 && Y_4 >= W_ * Y_13 * Y_4 && W_ * Y_15 * Y_6 + Y_15 >= 1 + Y_6 && Y_6 >= W_ * Y_15 * Y_6 && Y_16 >= Z_ && 2 * Y_16 + Y_16 * Y_17 >= 1 + Y_18 && Y_18 >= Y_16 + Y_16 * Y_17 && W_ * Y_17 + Y_17 >= 2 && 1 >= W_ * Y_17 && Y_18 * Y_19 + Y_18 >= 1 + Y_18 * Y_20 + Y_21 && Y_21 + Y_18 * Y_20 >= Y_18 * Y_19 && W_ * Y_20 * Y_5 + Y_20 >= 1 + Y_5 && Y_5 >= W_ * Y_20 * Y_5 && W_ * Y_19 * Y_4 + Y_19 >= 1 + Y_4 && Y_4 >= W_ * Y_19 * Y_4 && W_ * Y_21 * Y_6 + Y_21 >= 1 + Y_6 && Y_6 >= W_ * Y_21 * Y_6 && Y_ >= Y_22 && Y_22 * Y_23 + Y_22 >= 1 + Y_22 * Y_24 + Y_25 && Y_25 + Y_22 * Y_24 >= Y_22 * Y_23 && W_ * Y_24 * Y_5 + Y_24 >= 1 + Y_5 && Y_5 >= W_ * Y_24 * Y_5 && W_ * Y_23 * Y_4 + Y_23 >= 1 + Y_4 && Y_4 >= W_ * Y_23 * Y_4 && W_ * Y_25 * Y_6 + Y_25 >= 1 + Y_6 && Y_6 >= W_ * Y_25 * Y_6 && Y_26 >= Y_ && Y_26 * Y_27 + Y_26 >= 1 + Y_26 * Y_28 + Y_29 && Y_29 + Y_26 * Y_28 >= Y_26 * Y_27 && W_ * Y_28 * Y_5 + Y_28 >= 1 + Y_5 && Y_5 >= W_ * Y_28 * Y_5 && W_ * Y_27 * Y_4 + Y_27 >= 1 + Y_4 && Y_4 >= W_ * Y_27 * Y_4 && W_ * Y_29 * Y_6 + Y_29 >= 1 + Y_6 && Y_6 >= W_ * Y_29 * Y_6) { P = P_; Q = Q_; R = R_; S = S_; W = W_; X = X_; Y = Y_; Z = Z_; goto loc_f92; } } goto end; } loc_f8: { if (nondet_bool()) { int C_ = 1 + C; if (A >= C) { C = C_; goto loc_f8; } } if (nondet_bool()) { int B_ = 1 + B; if (C >= 1 + A) { B = B_; goto loc_f5; } } goto end; } loc_f80: { if (nondet_bool()) { int Y_10 = nondet(); int Y_0 = nondet(); int Y_1 = nondet(); int Y_2 = nondet(); int Y_3 = nondet(); int Y_4 = nondet(); int Y_5 = nondet(); int Y_6 = nondet(); int Y_7 = nondet(); int Y_8 = nondet(); int Y_9 = nondet(); int Z_ = nondet(); int Y_ = nondet(); int X_ = nondet(); int W_ = nondet(); int P_ = S * Y_10; if (Z_ >= Y_0 && 2 * Y_0 + Y_0 * Y_1 >= 1 + Y_2 && Y_2 >= Y_0 + Y_0 * Y_1 && W_ * Y_1 + Y_1 >= 2 && 1 >= W_ * Y_1 && S * W_ * Y_2 + Y_2 >= 1 + S && S >= S * W_ * Y_2 && Y_3 >= Z_ && 2 * Y_3 + Y_3 * Y_4 >= 1 + Y_5 && Y_5 >= Y_3 + Y_3 * Y_4 && W_ * Y_4 + Y_4 >= 2 && 1 >= W_ * Y_4 && S * W_ * Y_5 + Y_5 >= 1 + S && S >= S * W_ * Y_5 && Y_6 >= X_ && W_ * Y_6 + Y_6 >= 2 && 1 >= W_ * Y_6 && X_ >= Y_7 && W_ * Y_7 + Y_7 >= 2 && 1 >= W_ * Y_7 && Y_ >= Y_8 && S * W_ * Y_8 + Y_8 >= 1 + S && S >= S * W_ * Y_8 && Y_9 >= Y_ && S * W_ * Y_9 + Y_9 >= 1 + S && S >= S * W_ * Y_9 && T >= 0) { P = P_; W = W_; X = X_; Y = Y_; Z = Z_; goto loc_f92; } } if (nondet_bool()) { int Y_9 = nondet(); int Y_8 = nondet(); int Y_0 = nondet(); int Y_1 = nondet(); int Y_2 = nondet(); int Y_3 = nondet(); int Y_4 = nondet(); int Y_5 = nondet(); int Y_6 = nondet(); int Y_7 = nondet(); int Z_ = nondet(); int X_ = nondet(); int W_ = nondet(); int Y_ = -S * Y_8; int S_ = -S; int P_ = -S * Y_9; if (Y_0 >= Z_ && 2 * Y_0 + Y_0 * Y_1 + S * Y_2 >= 1 && 0 >= S * Y_2 + Y_0 + Y_0 * Y_1 && W_ * Y_1 + Y_1 >= 2 && 1 >= W_ * Y_1 && W_ * Y_2 + Y_2 >= 2 && 1 >= W_ * Y_2 && Z_ >= Y_3 && 2 * Y_3 + Y_3 * Y_4 + S * Y_5 >= 1 && 0 >= S * Y_5 + Y_3 + Y_3 * Y_4 && W_ * Y_4 + Y_4 >= 2 && 1 >= W_ * Y_4 && W_ * Y_5 + Y_5 >= 2 && 1 >= W_ * Y_5 && Y_6 >= X_ && W_ * Y_6 + Y_6 >= 2 && 1 >= W_ * Y_6 && X_ >= Y_7 && W_ * Y_7 + Y_7 >= 2 && 1 >= W_ * Y_7 && 0 >= 1 + T && W_ * Y_8 + Y_8 >= 2 && 1 >= W_ * Y_8) { P = P_; S = S_; W = W_; X = X_; Y = Y_; Z = Z_; goto loc_f92; } } goto end; } loc_f92: { if (nondet_bool()) { int P_ = nondet(); int K_ = nondet(); int A1_ = 1 + A1; if (B >= 1 + A1) { K = K_; P = P_; A1 = A1_; goto loc_f92; } } if (nondet_bool()) { if (A1 >= B) { goto loc_f101; } } goto end; } loc_f1: end: return 0; }