From e433951e27b8146f5d869c4b62213930c5ba974d Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 22 Mar 2023 17:44:02 +0100 Subject: [PATCH] Active lemmas need to be queued for repropagation after resetting conflict --- src/math/polysat/solver.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 17ad4f74d..3cc6830f3 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1437,8 +1437,14 @@ namespace polysat { unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes]; LOG_H3("Pop " << num_scopes << " user scopes"); pop_levels(m_level - base_level + 1); - if (m_level < m_conflict.level()) + if (m_level < m_conflict.level()) { + clause_ref_vector lemmas = m_conflict.take_lemmas(); m_conflict.reset(); + // TODO: currently we forget all new lemmas at this point. + for (clause* lemma : lemmas) + if (lemma->is_active()) + propagate_clause(*lemma); + } m_base_levels.shrink(m_base_levels.size() - num_scopes); m_base_index.shrink(m_base_index.size() - num_scopes); }