From 445546b684ceb512330e25f2a569dc11c0f05e6a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Sep 2018 17:20:40 -0700 Subject: [PATCH] fix gc Signed-off-by: Nikolaj Bjorner --- src/sat/ba_solver.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index acc3bbd21..88de3b6a1 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1570,6 +1570,7 @@ namespace sat { ++m_stats.m_num_resolves; ext_justification_idx index = js.get_ext_justification_idx(); constraint& cnstr = index2constraint(index); + SASSERT(!cnstr.was_removed()); switch (cnstr.tag()) { case card_t: case pb_t: { @@ -2660,7 +2661,8 @@ namespace sat { } void ba_solver::gc() { - if (m_learned.size() >= 2 * m_constraints.size()) { + if (m_learned.size() >= 2 * m_constraints.size() && + (s().at_search_lvl() || s().at_base_lvl())) { for (auto & c : m_learned) update_psm(*c); std::stable_sort(m_learned.begin(), m_learned.end(), constraint_glue_psm_lt()); gc_half("glue-psm");