diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp
index 7e40a002c..272a71fa4 100644
--- a/src/math/polysat/explain.cpp
+++ b/src/math/polysat/explain.cpp
@@ -49,6 +49,8 @@ namespace polysat {
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
+            if (si.is_resolved())
+                continue;
             auto c1 = s.lit2cnstr(si.lit());       
             if (!c1->contains_var(v))
                 continue;
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index 581c75f5b..e68d87a75 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -323,6 +323,8 @@ namespace polysat {
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
+            if (si.is_resolved())
+                continue;
             auto dd = s.lit2cnstr(si.lit());
             if (!dd->is_ule())
                 continue;
@@ -347,6 +349,8 @@ namespace polysat {
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
+            if (si.is_resolved())
+                continue;
             auto dd = s.lit2cnstr(si.lit());
             if (!dd->is_ule())
                 continue;
@@ -380,6 +384,8 @@ namespace polysat {
         for (auto si : s.m_search) {
             if (!si.is_boolean())
                 continue;
+            if (si.is_resolved())
+                continue;
             auto dd = s.lit2cnstr(si.lit());
             if (!dd->is_ule())
                 continue;
diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index f9cc96bcb..edac55526 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -32,6 +32,7 @@ namespace polysat {
             pvar m_var;
             sat::literal m_lit;
         };
+        bool m_resolved = false; // when marked as resolved it is no longer valid to reduce the conflict state
 
         search_item(pvar var): m_kind(search_item_k::assignment), m_var(var) {}
         search_item(sat::literal lit): m_kind(search_item_k::boolean), m_lit(lit) {}
@@ -40,9 +41,11 @@ namespace polysat {
         static search_item boolean(sat::literal lit) { return search_item(lit); }
         bool is_assignment() const { return m_kind == search_item_k::assignment; }
         bool is_boolean() const { return m_kind == search_item_k::boolean; }
+        bool is_resolved() const { return m_resolved; }
         search_item_k kind() const { return m_kind; }
         pvar var() const { SASSERT(is_assignment()); return m_var; }
         sat::literal lit() const { SASSERT(is_boolean()); return m_lit; }        
+        void set_resolved() { m_resolved = true; }
     };
 
     class search_state {
@@ -65,6 +68,8 @@ namespace polysat {
 
         void pop_asssignment();
 
+        void set_resolved(unsigned i) { m_items[i].set_resolved(); }
+
         using const_iterator = decltype(m_items)::const_iterator;
         const_iterator begin() const { return m_items.begin(); }
         const_iterator end() const { return m_items.end(); }
@@ -128,7 +133,11 @@ namespace polysat {
             init();
         }
 
-        search_item const& operator*() const {
+        void set_resolved() {
+            m_search->set_resolved(current);
+        }
+
+        search_item const& operator*() {
             return (*m_search)[current];
         }
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 53307ce23..65c0443db 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -477,7 +477,8 @@ namespace polysat {
         while (search_it.next()) {
             LOG("search state: " << m_search);
             LOG("Conflict: " << m_conflict);
-            auto const& item = *search_it;
+            auto& item = *search_it;
+            search_it.set_resolved();
             LOG_H2("Working on " << search_item_pp(m_search, item));
             if (item.is_assignment()) {
                 // Resolve over variable assignment