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) { goto loc_f0; loc_f0: { if (nondet_bool()) { int A_ = 1; if (A == 1) { A = A_; goto loc_f13; } } if (nondet_bool()) { int B_ = 1; if (0 >= A) { B = B_; goto loc_f17; } } if (nondet_bool()) { int B_ = 1; if (A >= 2) { B = B_; goto loc_f17; } } goto end; } loc_f17: { if (nondet_bool()) { int E_ = nondet(); int D_ = nondet(); int F_ = 1; int C_ = 1 + B; if (A >= B) { C = C_; D = D_; E = E_; F = F_; goto loc_f23; } } if (nondet_bool()) { if (B >= 1 + A) { goto loc_f13; } } goto end; } loc_f23: { if (nondet_bool()) { int E_ = nondet(); int D_ = nondet(); int F_ = 1 + F; if (B >= F) { D = D_; E = E_; F = F_; goto loc_f23; } } if (nondet_bool()) { int F_ = 1; if (F >= 1 + B && 0 >= 1 + E) { F = F_; goto loc_f33; } } if (nondet_bool()) { int F_ = 1; if (F >= 1 + B && E >= 1) { F = F_; goto loc_f33; } } if (nondet_bool()) { int F_ = 1; int E_ = 0; if (E == 0 && F >= 1 + B) { E = E_; F = F_; goto loc_f33; } } goto end; } loc_f33: { if (nondet_bool()) { int F_ = 1 + F; if (B >= F) { F = F_; goto loc_f33; } } if (nondet_bool()) { int C_ = A; if (A == C && F >= 1 + B) { C = C_; goto loc_f13; } } if (nondet_bool()) { int I_ = nondet(); int H_ = nondet(); int G_ = nondet(); int F_ = 1; if (F >= 1 + B && A >= 1 + C) { F = F_; G = G_; H = H_; I = I_; goto loc_f46; } } if (nondet_bool()) { int I_ = nondet(); int H_ = nondet(); int G_ = nondet(); int F_ = 1; if (F >= 1 + B && C >= 1 + A) { F = F_; G = G_; H = H_; I = I_; goto loc_f46; } } goto end; } loc_f46: { if (nondet_bool()) { int I_ = nondet(); int H_ = nondet(); int G_ = nondet(); int F_ = 1 + F; if (B >= F) { F = F_; G = G_; H = H_; I = I_; goto loc_f46; } } if (nondet_bool()) { int R_ = nondet(); int Q_ = nondet(); int J_ = nondet(); int K_ = B; int F_ = 1; if (F >= 1 + B) { F = F_; J = J_; K = K_; Q = Q_; R = R_; goto loc_f60; } } goto end; } loc_f60: { if (nondet_bool()) { int O_ = nondet(); int N_ = nondet(); int M_ = nondet(); int L_ = nondet(); int P_ = K; int K_ = -1 + K; int F_ = 1 + F; if (J >= F) { F = F_; K = K_; L = L_; M = M_; N = N_; O = O_; P = P_; goto loc_f60; } } if (nondet_bool()) { int B_ = 1 + B; if (F >= 1 + J) { B = B_; goto loc_f17; } } goto end; } loc_f13: end: return 0; }