diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 5ba5e135d..55cc088f4 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -225,7 +225,6 @@ namespace smt { recfun::vars const & vars, expr_ref_vector const & args, expr * e) { - SASSERT(is_standard_order(vars)); var_subst subst(m, true); expr_ref new_body = subst(e, args); ctx.get_rewriter()(new_body); // simplify @@ -377,7 +376,6 @@ namespace smt { recfun::def & d = *e.m_cdef->get_def(); auto & vars = d.get_vars(); auto & args = e.m_args; - SASSERT(is_standard_order(vars)); unsigned depth = get_depth(e.m_pred); expr_ref lhs(u().mk_fun_defined(d, args), m); expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs()); diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index 2e576a29a..7ca25f917 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -82,7 +82,7 @@ namespace smt { void set_depth_rec(unsigned d, expr* e); literal mk_eq_lit(expr* l, expr* r); - bool is_standard_order(recfun::vars const& vars) const { + bool is_decreasing_order(recfun::vars const& vars) const { return vars.empty() || vars[vars.size()-1]->get_idx() == 0; } protected: