diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 6e052f3d8..4c08c4c75 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -380,8 +380,9 @@ namespace polysat {
 #endif
 
         if (!has_decision) {
+            unsigned const eval_idx = s.m_search.get_bool_index(lit);
             for (pvar v : c->vars()) {
-                if (s.is_assigned(v) && s.get_level(v) <= lvl) {
+                if (s.is_assigned(v) && s.m_search.get_pvar_index(v) <= eval_idx) {
                     m_vars.insert(v);
 // TODO - figure out what to do with constraints from conflict lemma that disappear here.
 //                    if (s.m_bvars.is_false(lit))
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index 6eb8e9131..0bfbcfd62 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -101,15 +101,27 @@ namespace polysat {
         return false;
     }
 
-    void search_state::push_assignment(pvar p, rational const& r) {
-        m_items.push_back(search_item::assignment(p));
-        m_assignment.push(p, r);
+    void search_state::push_assignment(pvar v, rational const& r) {
+        m_pvar_to_idx.setx(v, m_items.size(), UINT_MAX);
+        m_items.push_back(search_item::assignment(v));
+        m_assignment.push(v, r);
     }
 
     void search_state::push_boolean(sat::literal lit) {
+        m_bool_to_idx.setx(lit.var(), m_items.size(), UINT_MAX);
         m_items.push_back(search_item::boolean(lit));
     }
 
+    unsigned search_state::get_pvar_index(pvar v) const {
+        SASSERT(s.is_assigned(v));
+        return m_pvar_to_idx[v];
+    }
+
+    unsigned search_state::get_bool_index(sat::bool_var var) const {
+        SASSERT(s.m_bvars.is_assigned(var));
+        return m_bool_to_idx[var];
+    }
+
     void search_state::pop() {
         auto const& item = m_items.back();
         if (item.is_assignment()) {
diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index 3c06b2781..379ac43e8 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -51,6 +51,10 @@ namespace polysat {
         vector<search_item> m_items;
         assignment          m_assignment;
 
+        // store index into m_items
+        unsigned_vector     m_pvar_to_idx;
+        unsigned_vector     m_bool_to_idx;
+
         bool value(pvar v, rational& r) const;
 
     public:
@@ -67,10 +71,14 @@ namespace polysat {
         //       (update on set_resolved? might be one iteration too early, looking at the old solver::resolve_conflict loop)
         substitution const& unresolved_assignment(unsigned sz) const;
 
-        void push_assignment(pvar p, rational const& r);
+        void push_assignment(pvar v, rational const& r);
         void push_boolean(sat::literal lit);
         void pop();
 
+        unsigned get_pvar_index(pvar v) const;
+        unsigned get_bool_index(sat::bool_var var) const;
+        unsigned get_bool_index(sat::literal lit) const { return get_bool_index(lit.var()); }
+
         void set_resolved(unsigned i) { m_items[i].set_resolved(); }
 
         using const_iterator = decltype(m_items)::const_iterator;