From b0787024c72f8966004df580002ca2e7de8f83b3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Mar 2013 09:47:52 -0700 Subject: [PATCH] Move ast_counter to location for common utilities. It depends on get_free_vars, so is in rewriter directory Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_compiler.cpp | 4 +- src/muz_qe/dl_mk_explanations.cpp | 4 +- src/muz_qe/dl_mk_interp_tail_simplifier.cpp | 6 +- src/muz_qe/dl_mk_karr_invariants.cpp | 2 +- src/muz_qe/dl_mk_rule_inliner.cpp | 8 +- src/muz_qe/dl_mk_similarity_compressor.cpp | 6 +- src/muz_qe/dl_mk_simple_joins.cpp | 4 +- src/muz_qe/dl_rule.cpp | 2 +- src/muz_qe/dl_rule.h | 4 +- src/muz_qe/dl_util.cpp | 150 +----------------- src/muz_qe/dl_util.h | 84 +--------- src/muz_qe/pdr_context.cpp | 6 +- src/muz_qe/pdr_quantifiers.cpp | 4 +- src/muz_qe/tab_context.cpp | 2 +- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 54 +++++-- 15 files changed, 78 insertions(+), 262 deletions(-) diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 44a449779..cc56df4b7 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -384,8 +384,8 @@ namespace datalog { void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) { SASSERT(r->get_positive_tail_size()==2); ast_manager & m = m_context.get_manager(); - var_counter counter; - counter.count_vars(m, r); + rule_counter counter; + counter.count_rule_vars(m, r); app * t1 = r->get_tail(0); app * t2 = r->get_tail(1); counter.count_vars(m, t1, -1); diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp index b4683bdbe..464ec838e 100644 --- a/src/muz_qe/dl_mk_explanations.cpp +++ b/src/muz_qe/dl_mk_explanations.cpp @@ -708,8 +708,8 @@ namespace datalog { } rule * mk_explanations::get_e_rule(rule * r) { - var_counter ctr; - ctr.count_vars(m_manager, r); + rule_counter ctr; + ctr.count_rule_vars(m_manager, r); unsigned max_var; unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0; unsigned head_var = next_var++; diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp index d028c8751..d1b7f15dd 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp @@ -35,7 +35,7 @@ namespace datalog { // ----------------------------------- void mk_interp_tail_simplifier::rule_substitution::reset(rule * r) { - unsigned var_cnt = m_context.get_rule_manager().get_var_counter().get_max_var(*r)+1; + unsigned var_cnt = m_context.get_rule_manager().get_counter().get_max_rule_var(*r)+1; m_subst.reset(); m_subst.reserve(1, var_cnt); m_rule = r; @@ -541,8 +541,8 @@ namespace datalog { rule_ref pro_var_eq_result(m_context.get_rule_manager()); if (propagate_variable_equivalences(res, pro_var_eq_result)) { - SASSERT(var_counter().get_max_var(*r.get())==0 || - var_counter().get_max_var(*r.get()) > var_counter().get_max_var(*pro_var_eq_result.get())); + SASSERT(rule_counter().get_max_rule_var(*r.get())==0 || + rule_counter().get_max_rule_var(*r.get()) > rule_counter().get_max_rule_var(*pro_var_eq_result.get())); r = pro_var_eq_result; goto start; } diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index f690346bc..9c034c890 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -145,7 +145,7 @@ namespace datalog { } bool mk_karr_invariants::get_transition_relation(rule const& r, matrix& M) { - unsigned num_vars = rm.get_var_counter().get_max_var(r)+1; + unsigned num_vars = rm.get_counter().get_max_rule_var(r)+1; unsigned arity = r.get_decl()->get_arity(); unsigned num_columns = arity + num_vars; unsigned utsz = r.get_uninterpreted_tail_size(); diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index 0919e2ff0..1404c9c8c 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -65,8 +65,8 @@ namespace datalog { // ----------------------------------- bool rule_unifier::unify_rules(const rule& tgt, unsigned tgt_idx, const rule& src) { - var_counter& vc = m_rm.get_var_counter(); - unsigned var_cnt = std::max(vc.get_max_var(tgt), vc.get_max_var(src))+1; + rule_counter& vc = m_rm.get_counter(); + unsigned var_cnt = std::max(vc.get_max_rule_var(tgt), vc.get_max_rule_var(src))+1; m_subst.reset(); m_subst.reserve(2, var_cnt); @@ -733,7 +733,7 @@ namespace datalog { } // initialize substitution. - var_counter& vc = m_rm.get_var_counter(); + rule_counter& vc = m_rm.get_counter(); unsigned max_var = 0; for (unsigned i = 0; i < sz; ++i) { rule* r = acc[i].get(); @@ -820,7 +820,7 @@ namespace datalog { del_rule(r2, j); } - max_var = std::max(max_var, vc.get_max_var(*r.get())); + max_var = std::max(max_var, vc.get_max_rule_var(*r.get())); m_subst.reserve_vars(max_var+1); } diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp index 42a5ba367..a040a623a 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.cpp +++ b/src/muz_qe/dl_mk_similarity_compressor.cpp @@ -372,10 +372,10 @@ namespace datalog { new_negs.push_back(r->is_neg_tail(i)); } - var_counter var_ctr; - var_ctr.count_vars(m_manager, r); + rule_counter ctr; + ctr.count_rule_vars(m_manager, r); unsigned max_var_idx, new_var_idx_base; - if(var_ctr.get_max_positive(max_var_idx)) { + if(ctr.get_max_positive(max_var_idx)) { new_var_idx_base = max_var_idx+1; } else { diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp index 363a4f0f7..77c6c2951 100644 --- a/src/muz_qe/dl_mk_simple_joins.cpp +++ b/src/muz_qe/dl_mk_simple_joins.cpp @@ -310,8 +310,8 @@ namespace datalog { } void register_rule(rule * r) { - var_counter counter; - counter.count_vars(m, r, 1); + rule_counter counter; + counter.count_rule_vars(m, r, 1); ptr_vector & rule_content = m_rules_content.insert_if_not_there2(r, ptr_vector())->get_data().m_value; diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index 3814d0b62..de41e4774 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -705,7 +705,7 @@ namespace datalog { bool_rewriter(m).mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr(), unbound_tail); unsigned q_var_cnt = unbound_vars.num_elems(); - unsigned max_var = m_var_counter.get_max_var(*r); + unsigned max_var = m_counter.get_max_rule_var(*r); expr_ref_vector subst(m); diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h index c01b36162..4afc08edb 100644 --- a/src/muz_qe/dl_rule.h +++ b/src/muz_qe/dl_rule.h @@ -45,7 +45,7 @@ namespace datalog { { ast_manager& m; context& m_ctx; - var_counter m_var_counter; + rule_counter m_counter; obj_map m_memoize_disj; expr_ref_vector m_refs; @@ -162,7 +162,7 @@ namespace datalog { static bool is_forall(ast_manager& m, expr* e, quantifier*& q); - var_counter& get_var_counter() { return m_var_counter; } + rule_counter& get_counter() { return m_counter; } }; diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp index 4a406578c..bde03e765 100644 --- a/src/muz_qe/dl_util.cpp +++ b/src/muz_qe/dl_util.cpp @@ -431,89 +431,8 @@ namespace datalog { } } - void counter::update(unsigned el, int delta) { - int & counter = get(el); - SASSERT(!m_stay_non_negative || counter>=0); - SASSERT(!m_stay_non_negative || static_cast(counter)>=-delta); - counter += delta; - } - - int & counter::get(unsigned el) { - return m_data.insert_if_not_there2(el, 0)->get_data().m_value; - } - - counter & counter::count(unsigned sz, const unsigned * els, int delta) { - for(unsigned i=0; im_value>0 ) { - cnt++; - } - } - return cnt; - } - - void counter::collect_positive(idx_set & acc) const { - iterator eit = begin(); - iterator eend = end(); - for(; eit!=eend; ++eit) { - if(eit->m_value>0) { acc.insert(eit->m_key); } - } - } - - bool counter::get_max_positive(unsigned & res) const { - bool found = false; - iterator eit = begin(); - iterator eend = end(); - for(; eit!=eend; ++eit) { - if( eit->m_value>0 && (!found || eit->m_key>res) ) { - found = true; - res = eit->m_key; - } - } - return found; - } - - unsigned counter::get_max_positive() const { - unsigned max_pos; - VERIFY(get_max_positive(max_pos)); - return max_pos; - } - - int counter::get_max_counter_value() const { - int res = 0; - iterator eit = begin(); - iterator eend = end(); - for (; eit!=eend; ++eit) { - if( eit->m_value>res ) { - res = eit->m_value; - } - } - return res; - } - - void var_counter::count_vars(ast_manager & m, const app * pred, int coef) { - unsigned n = pred->get_num_args(); - for (unsigned i = 0; i < n; i++) { - m_sorts.reset(); - ::get_free_vars(pred->get_arg(i), m_sorts); - for (unsigned j = 0; j < m_sorts.size(); ++j) { - if (m_sorts[j]) { - update(j, coef); - } - } - } - } - - void var_counter::count_vars(ast_manager & m, const rule * r, int coef) { + + void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) { count_vars(m, r->get_head(), 1); unsigned n = r->get_tail_size(); for (unsigned i = 0; i < n; i++) { @@ -521,50 +440,7 @@ namespace datalog { } } - unsigned var_counter::get_max_var(bool& has_var) { - has_var = false; - unsigned max_var = 0; - while (!m_todo.empty()) { - expr* e = m_todo.back(); - unsigned scope = m_scopes.back(); - m_todo.pop_back(); - m_scopes.pop_back(); - if (m_visited.is_marked(e)) { - continue; - } - m_visited.mark(e, true); - switch(e->get_kind()) { - case AST_QUANTIFIER: { - quantifier* q = to_quantifier(e); - m_todo.push_back(q->get_expr()); - m_scopes.push_back(scope + q->get_num_decls()); - break; - } - case AST_VAR: { - if (to_var(e)->get_idx() >= scope + max_var) { - has_var = true; - max_var = to_var(e)->get_idx() - scope; - } - break; - } - case AST_APP: { - app* a = to_app(e); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - m_todo.push_back(a->get_arg(i)); - m_scopes.push_back(scope); - } - break; - } - default: - UNREACHABLE(); - break; - } - } - m_visited.reset(); - return max_var; - } - - unsigned var_counter::get_max_var(const rule & r) { + unsigned rule_counter::get_max_rule_var(const rule & r) { m_todo.push_back(r.get_head()); m_scopes.push_back(0); unsigned n = r.get_tail_size(); @@ -576,22 +452,6 @@ namespace datalog { return get_max_var(has_var); } - unsigned var_counter::get_max_var(expr* e) { - bool has_var = false; - m_todo.push_back(e); - m_scopes.push_back(0); - return get_max_var(has_var); - } - - unsigned var_counter::get_next_var(expr* e) { - bool has_var = false; - m_todo.push_back(e); - m_scopes.push_back(0); - unsigned mv = get_max_var(has_var); - if (has_var) mv++; - return mv; - } - void del_rule(horn_subsume_model_converter* mc, rule& r) { if (mc) { ast_manager& m = mc->get_manager(); @@ -678,10 +538,6 @@ namespace datalog { proof_converter* mk_skip_proof_converter() { return alloc(skip_proof_converter); } - unsigned get_max_var(const rule & r, ast_manager & m) { - var_counter ctr; - return ctr.get_max_var(r); - } void reverse_renaming(ast_manager & m, const expr_ref_vector & src, expr_ref_vector & tgt) { SASSERT(tgt.empty()); diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index 69be7e9ac..45d327d44 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -27,6 +27,7 @@ Revision History: #include"replace_proof_converter.h" #include"substitution.h" #include"fixedpoint_params.hpp" +#include"ast_counter.h" namespace datalog { @@ -411,80 +412,12 @@ namespace datalog { } - class counter { - protected: - typedef u_map map_impl; - map_impl m_data; - const bool m_stay_non_negative; + + class rule_counter : public var_counter { public: - typedef map_impl::iterator iterator; - - counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {} - - iterator begin() const { return m_data.begin(); } - iterator end() const { return m_data.end(); } - - void update(unsigned el, int delta); - int & get(unsigned el); - /** - \brief Increase values of elements in \c els by \c delta. - - The function returns a reference to \c *this to allow for expressions like - counter().count(sz, arr).get_positive_count() - */ - counter & count(unsigned sz, const unsigned * els, int delta = 1); - counter & count(const unsigned_vector & els, int delta = 1) { - return count(els.size(), els.c_ptr(), delta); - } - - void collect_positive(idx_set & acc) const; - unsigned get_positive_count() const; - bool get_max_positive(unsigned & res) const; - unsigned get_max_positive() const; - /** - Since the default counter value of a counter is zero, the result is never negative. - */ - int get_max_counter_value() const; - }; - - class var_counter : public counter { - ptr_vector m_sorts; - expr_fast_mark1 m_visited; - ptr_vector m_todo; - unsigned_vector m_scopes; - unsigned get_max_var(bool & has_var); - - public: - var_counter(bool stay_non_negative = true) : counter(stay_non_negative) {} - void count_vars(ast_manager & m, const app * t, int coef = 1); - void count_vars(ast_manager & m, const rule * r, int coef = 1); - unsigned get_max_var(const rule& r); - unsigned get_max_var(expr* e); - unsigned get_next_var(expr* e); - }; - - class ast_counter { - typedef obj_map map_impl; - map_impl m_data; - bool m_stay_non_negative; - public: - typedef map_impl::iterator iterator; - - ast_counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {} - - iterator begin() const { return m_data.begin(); } - iterator end() const { return m_data.end(); } - - int & get(ast * el) { - return m_data.insert_if_not_there2(el, 0)->get_data().m_value; - } - void update(ast * el, int delta){ - get(el)+=delta; - SASSERT(!m_stay_non_negative || get(el)>=0); - } - - void inc(ast * el) { update(el, 1); } - void dec(ast * el) { update(el, -1); } + rule_counter(bool stay_non_negative = true): var_counter(stay_non_negative) {} + void count_rule_vars(ast_manager & m, const rule * r, int coef = 1); + unsigned get_max_rule_var(const rule& r); }; void del_rule(horn_subsume_model_converter* mc, rule& r); @@ -497,11 +430,6 @@ namespace datalog { proof_converter* mk_skip_proof_converter(); - /** - Return maximal variable number, or zero is there isn't any - */ - // unsigned get_max_var(const rule & r, ast_manager & m); - void reverse_renaming(ast_manager & m, const expr_ref_vector & src, expr_ref_vector & tgt); /** diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 8bdff1800..d6718c33c 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -968,11 +968,11 @@ namespace pdr { unsigned deltas[2]; datalog::rule_ref rule(rm), r0(rm); model_node* n = m_root; - datalog::var_counter& vc = rm.get_var_counter(); + datalog::rule_counter& vc = rm.get_counter(); substitution subst(m); unifier unif(m); rule = n->get_rule(); - unsigned max_var = vc.get_max_var(*rule); + unsigned max_var = vc.get_max_rule_var(*rule); predicates.push_back(rule->get_head()); children.append(n); bool first = true; @@ -983,7 +983,7 @@ namespace pdr { children.pop_back(); n->mk_instantiate(r0, rule, binding); - max_var = std::max(max_var, vc.get_max_var(*rule)); + max_var = std::max(max_var, vc.get_max_rule_var(*rule)); subst.reset(); subst.reserve(2, max_var+1); deltas[0] = 0; diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index 5cc97893a..4a7b4b995 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -612,8 +612,8 @@ namespace pdr { datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end(); for (; it != end; ++it) { datalog::rule* r = *it; - datalog::var_counter vc(true); - unsigned max_var = vc.get_max_var(*r); + datalog::rule_counter vc(true); + unsigned max_var = vc.get_max_rule_var(*r); app_ref_vector body(m); for (unsigned i = 0; i < m_instantiations.size(); ++i) { if (r == m_instantiated_rules[i]) { diff --git a/src/muz_qe/tab_context.cpp b/src/muz_qe/tab_context.cpp index 72727bea8..681d3d4b2 100644 --- a/src/muz_qe/tab_context.cpp +++ b/src/muz_qe/tab_context.cpp @@ -317,7 +317,7 @@ namespace tb { for (unsigned i = utsz; i < tsz; ++i) { fmls.push_back(r->get_tail(i)); } - m_num_vars = 1 + r.get_manager().get_var_counter().get_max_var(*r); + m_num_vars = 1 + r.get_manager().get_counter().get_max_rule_var(*r); m_head = r->get_head(); m_predicates.reset(); for (unsigned i = 0; i < utsz; ++i) { diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 25c41c2a2..0092cdd38 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -92,7 +92,34 @@ protected: ptr_vector fmls; g.get_formulas(fmls); fml = m.mk_and(fmls.size(), fmls.c_ptr()); + m_solver.push(); reduce(fml); + m_solver.pop(1); + SASSERT(m_solver.get_scope_level() == 0); + TRACE("ctx_solver_simplify_tactic", + for (unsigned i = 0; i < fmls.size(); ++i) { + tout << mk_pp(fmls[i], m) << "\n"; + } + tout << "=>\n"; + tout << mk_pp(fml, m) << "\n";); + DEBUG_CODE( + { + m_solver.push(); + expr_ref fml1(m); + fml1 = m.mk_and(fmls.size(), fmls.c_ptr()); + fml1 = m.mk_iff(fml, fml1); + fml1 = m.mk_not(fml1); + m_solver.assert_expr(fml1); + lbool is_sat = m_solver.check(); + TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";); + if (is_sat != l_false) { + TRACE("ctx_solver_simplify_tactic", + tout << "result is not equivalent to input\n"; + tout << mk_pp(fml1, m) << "\n";); + UNREACHABLE(); + } + m_solver.pop(1); + }); g.reset(); g.assert_expr(fml, 0, 0); IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-solver-simplify :num-steps " << m_num_steps << ")\n";); @@ -106,21 +133,22 @@ protected: svector is_checked; svector parent_ids, self_ids; expr_ref_vector fresh_vars(m), trail(m); - expr_ref res(m); + expr_ref res(m), tmp(m); obj_map > cache; unsigned id = 1; - expr* n = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true)); expr* n2, *fml; unsigned path_id = 0, self_pos = 0; app * a; unsigned sz; std::pair path_r; ptr_vector found; + expr* n = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true)); + trail.push_back(n); fml = result.get(); - m_solver.assert_expr(m.mk_not(m.mk_iff(fml, n))); + tmp = m.mk_not(m.mk_iff(fml, n)); + m_solver.assert_expr(tmp); - trail.push_back(n); todo.push_back(fml); names.push_back(n); is_checked.push_back(false); @@ -144,6 +172,7 @@ protected: goto done; } if (m.is_bool(e) && !checked && simplify_bool(n, res)) { + TRACE("ctx_solver_simplify_tactic", tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";); goto done; } if (!is_app(e)) { @@ -176,7 +205,7 @@ protected: found.push_back(arg); if (path_r.first == self_pos) { - TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << "\n";); + TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << " |-> " << mk_pp(path_r.second, m) << "\n";); args.push_back(path_r.second); } else { @@ -188,11 +217,11 @@ protected: } else if (!n2 && !found.contains(arg)) { n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true)); + trail.push_back(n2); todo.push_back(arg); parent_ids.push_back(self_pos); self_ids.push_back(0); names.push_back(n2); - trail.push_back(n2); args.push_back(n2); is_checked.push_back(false); } @@ -205,7 +234,8 @@ protected: // child needs to be visited. if (n2) { m_solver.push(); - m_solver.assert_expr(m.mk_eq(res, n)); + tmp = m.mk_eq(res, n); + m_solver.assert_expr(tmp); continue; } @@ -229,7 +259,7 @@ protected: } bool simplify_bool(expr* n, expr_ref& res) { - + expr_ref tmp(m); m_solver.push(); m_solver.assert_expr(n); lbool is_sat = m_solver.check(); @@ -240,7 +270,8 @@ protected: } m_solver.push(); - m_solver.assert_expr(m.mk_not(n)); + tmp = m.mk_not(n); + m_solver.assert_expr(tmp); is_sat = m_solver.check(); m_solver.pop(1); if (is_sat == l_false) { @@ -254,7 +285,7 @@ protected: expr_ref local_simplify(app* a, expr* n, unsigned& id, unsigned index) { SASSERT(index < a->get_num_args()); SASSERT(m.is_bool(a->get_arg(index))); - expr_ref n2(m), result(m); + expr_ref n2(m), result(m), tmp(m); n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true)); ptr_buffer args; for (unsigned i = 0; i < a->get_num_args(); ++i) { @@ -267,7 +298,8 @@ protected: } m_mk_app(a->get_decl(), args.size(), args.c_ptr(), result); m_solver.push(); - m_solver.assert_expr(m.mk_eq(result, n)); + tmp = m.mk_eq(result, n); + m_solver.assert_expr(tmp); if (!simplify_bool(n2, result)) { result = a; }