fix conflict reset condition

src/math/polysat/conflict.cpp

@@ -192,6 +192,7 @@ namespace polysat {
     }
 
     unsigned conflict::effective_level() const {
+        SASSERT(!empty());
         // If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier.
         if (m_dep != null_dependency)
             return m_level;
@@ -207,6 +208,22 @@ namespace polysat {
         return lvl;
     }
 
+    bool conflict::is_valid() const {
+        SASSERT(!empty());
+        // If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier.
+        if (m_dep != null_dependency)
+            return m_level <= s.m_level;
+        // All conflict constraints must be bool-assigned.
+        for (unsigned lit_idx : m_literals)
+            if (!s.m_bvars.is_assigned(sat::to_literal(lit_idx)))
+                return false;
+        // All conflict variables must be assigned.
+        for (pvar v : m_vars)
+            if (!s.is_assigned(v))
+                return false;
+        return true;
+    }
+
     void conflict::init_at_base_level(dependency dep) {
         SASSERT(empty());
         SASSERT(s.at_base_level());

src/math/polysat/conflict.h

@@ -123,6 +123,7 @@ namespace polysat {
 
         unsigned level() const { return m_level; }
         unsigned effective_level() const;
+        bool is_valid() const;  // TODO: better name?
 
         bool is_relevant_pvar(pvar v) const;
         bool is_relevant(sat::literal lit) const;

src/math/polysat/solver.cpp

@@ -1439,20 +1439,35 @@ namespace polysat {
         unsigned const base_level = m_base_levels[m_base_levels.size() - num_scopes];
         unsigned const target_level = base_level - 1;
 
-        clause_ref_vector lemmas;
+        // TODO: effective_level is the wrong measure (or rather, we would need additional work to be able to keep the conflict).
-        if (is_conflict() && target_level < m_conflict.effective_level()) {
+        //       we should compare m_search index. Alternatively, simply check if pop_levels unassigned any relevant element.
-            lemmas = m_conflict.take_lemmas();
+        // clause_ref_vector lemmas;
-            m_conflict.reset();
+        // if (is_conflict() && target_level < m_conflict.effective_level()) {
+        //     lemmas = m_conflict.take_lemmas();
+        //     m_conflict.reset();
+        // }
+        if (is_conflict()) {
+            for (signed_constraint c : m_conflict) {
+                VERIFY(m_bvars.is_assigned(c.blit()));
+            }
+            for (pvar v : m_conflict.vars()) {
+                VERIFY(is_assigned(v));
+            }
+            VERIFY(m_conflict.is_valid());
         }
 
         pop_levels(m_level - base_level + 1);
         SASSERT_EQ(m_level, target_level);
 
+        if (is_conflict() && !m_conflict.is_valid()) {
+            clause_ref_vector lemmas = m_conflict.take_lemmas();
+            m_conflict.reset();
             // TODO: currently we forget all new lemmas at this point.
             //       (but anything that uses popped assumptions cannot be used anymore.)
             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);