diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index b11b945fd..b920eaa89 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -375,10 +375,7 @@ namespace recfun { SASSERT(n_vars == d->get_arity()); is_imm_pred is_i(*u); -#if 0 - expr_ref reduced_rhs = preprocess_ites(*u, r, n_vars, vars, rhs); - d->compute_cases(*u, r, is_i, n_vars, vars, reduced_rhs); -#endif + d->compute_cases(*u, r, is_i, n_vars, vars, rhs); } namespace decl {