From d1d64bbe599cb1634df86b87215a78a6ccbdbb0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Aug 2021 04:55:20 -0700 Subject: [PATCH] #5454 --- src/sat/sat_simplifier.cpp | 12 ++++++++---- .../portfolio/solver_subsumption_tactic.cpp | 16 ++++++++-------- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 7a695746738..a9910852ee7 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -2022,10 +2022,14 @@ namespace sat { } remove_bin_clauses(pos_l); remove_bin_clauses(neg_l); - remove_clauses(pos_occs, pos_l); - remove_clauses(neg_occs, neg_l); - pos_occs.reset(); - neg_occs.reset(); + { + clause_use_list& pos_occs = m_use_list.get(pos_l); + clause_use_list& neg_occs = m_use_list.get(neg_l); + remove_clauses(pos_occs, pos_l); + remove_clauses(neg_occs, neg_l); + pos_occs.reset(); + neg_occs.reset(); + } return true; } diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index 5a4de001f9d..3a23f598467 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -53,7 +53,7 @@ class solver_subsumption_tactic : public tactic { */ bool simplify(expr_ref& f) { - expr_ref_vector fmls(m), ors(m), nprefix(m), prefix(m); + expr_ref_vector fmls(m), ors(m), nors(m), prefix(m); expr_ref nf(m.mk_not(f), m); fmls.push_back(nf); lbool is_sat = m_solver->check_sat(fmls); @@ -65,15 +65,15 @@ class solver_subsumption_tactic : public tactic { return false; ors.append(to_app(f)->get_num_args(), to_app(f)->get_args()); for (expr* arg : ors) - nprefix.push_back(mk_not(m, arg)); + nors.push_back(mk_not(m, arg)); for (unsigned i = 0; i < ors.size(); ++i) { expr* arg = ors.get(i); - expr_ref save(nprefix.get(i), m); - nprefix[i] = arg; - is_sat = m_solver->check_sat(nprefix); - nprefix[i] = save; + expr_ref save(nors.get(i), m); + nors[i] = arg; + is_sat = m_solver->check_sat(nors); + nors[i] = save; if (is_sat == l_false) - nprefix[i] = m.mk_true(); + nors[i] = m.mk_true(); else prefix.push_back(arg); } @@ -141,7 +141,7 @@ class solver_subsumption_tactic : public tactic { } void collect_param_descrs(param_descrs& r) override { - r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call."); + r.insert("max_conflicts", CPK_UINT, "(default: 2) maximal number of conflicts allowed per solver call."); } void operator()(goal_ref const& g, goal_ref_buffer& result) override {