From a4c3a8c6401aa632ab897653f884d30632d08f02 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 13 Sep 2021 16:01:22 +0200
Subject: [PATCH] more fixes

---
 src/math/polysat/conflict_core.cpp | 9 ++++++---
 src/math/polysat/search_state.h    | 8 ++++----
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp
index f1ee46c16..2a9c15be0 100644
--- a/src/math/polysat/conflict_core.cpp
+++ b/src/math/polysat/conflict_core.cpp
@@ -136,6 +136,7 @@ namespace polysat {
     }
 
     void conflict_core::remove_var(pvar v) {
+        LOG("Removing v" << v << " from core");
         unsigned j = 0;
         for (unsigned i = 0; i < m_constraints.size(); ++i)
             if (m_constraints[i]->contains_var(v))
@@ -146,8 +147,10 @@ namespace polysat {
         indexed_uint_set literals_copy = m_literals;  // TODO: can avoid copy (e.g., add a filter method for indexed_uint_set)
         for (unsigned lit_idx : literals_copy) {
             signed_constraint c = cm().lookup(sat::to_literal(lit_idx));
-            if (c->contains_var(v))
+            if (c->contains_var(v)) {
                 unset_mark(c);
+                m_literals.remove(lit_idx);
+            }
         }
         m_vars.remove(v);
     }
@@ -188,9 +191,9 @@ namespace polysat {
     /** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
     void conflict_core::keep(signed_constraint c) {
         if (!c->has_bvar()) {
-            m_constraints.erase(c);
+            remove(c);
             cm().ensure_bvar(c.get());
-            insert_literal(c.blit());
+            insert(c);
         }
         LOG_H3("keeping: " << c);
         // NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index c2c80ad99..014881c12 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -92,7 +92,7 @@ namespace polysat {
 
         void init() {
             first = m_search->size();
-            current = first - 1;
+            current = first;  // we start one before the beginning
         }
 
         void try_push_block() {
@@ -104,7 +104,8 @@ namespace polysat {
 
         void pop_block() {
             current = m_index_stack.back().current;
-            first = m_index_stack.back().first;
+            // We don't restore 'first', otherwise 'next()' will immediately push a new block again.
+            // Instead, the current block is merged with the popped one.
             m_index_stack.pop_back();
         }
 
@@ -116,7 +117,6 @@ namespace polysat {
         search_iterator(search_state& search):
             m_search(&search) {
             init();
-            current++;  // we start one before the beginning, then it also works for empty m_search
         }
 
         search_item const& operator*() const {
@@ -134,7 +134,7 @@ namespace polysat {
                 if (m_index_stack.empty())
                     return false;
                 pop_block();
-                return true;
+                return next();
             }
         }
     };