diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 7d8ffc0aa..eccc156de 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1001,6 +1001,14 @@ void pred_transformer::init_rules(decl2rel const& pts, expr_ref& init, expr_ref& } } +static bool is_all_non_null(app_ref_vector const& v) +{ + for (unsigned i = 0; i < v.size(); ++i) { + if (!v[i]) { return false; } + } + return true; +} + void pred_transformer::init_rule( decl2rel const& pts, datalog::rule const& rule, @@ -1035,7 +1043,7 @@ void pred_transformer::init_rule( fml = mk_and (tail); ground_free_vars (fml, var_reprs, aux_vars, ut_size == 0); - SASSERT(check_filled(var_reprs)); + SASSERT(is_all_non_null(var_reprs)); expr_ref tmp(m); var_subst (m, false)(fml, @@ -1074,13 +1082,6 @@ void pred_transformer::init_rule( tout << "\n";); } -bool pred_transformer::check_filled(app_ref_vector const& v) const -{ - for (unsigned i = 0; i < v.size(); ++i) { - if (!v[i]) { return false; } - } - return true; -} // create constants for free variables in tail. void pred_transformer::ground_free_vars(expr* e, app_ref_vector& vars, diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 9d3456f2b..0d4db2279 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -320,8 +320,6 @@ class pred_transformer { void simplify_formulas(tactic& tac, expr_ref_vector& fmls); // Debugging - bool check_filled(app_ref_vector const& v) const; - void add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r); expr* mk_fresh_reach_case_var ();