diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 4ad1069b9..cb431fe94 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -147,6 +147,7 @@ namespace polysat {
             SASSERT(m_literals.empty());
             SASSERT(m_vars.empty());
             SASSERT(m_bail_vars.empty());
+            SASSERT(m_vars_occurring.empty());
             SASSERT(m_lemmas.empty());
             SASSERT(m_narrow_queue.empty());
         }
@@ -159,6 +160,7 @@ namespace polysat {
         m_bail_vars.reset();
         m_relevant_vars.reset();
         m_var_occurrences.reset();
+        m_vars_occurring.reset();
         m_lemmas.reset();
         m_narrow_queue.reset();
         m_kind = conflict_kind_t::ok;
@@ -302,6 +304,8 @@ namespace polysat {
         for (pvar v : c->vars()) {
             if (v >= m_var_occurrences.size())
                 m_var_occurrences.resize(v + 1, 0);
+            if (!m_var_occurrences[v])
+                m_vars_occurring.insert(v);
             m_var_occurrences[v]++;
         }
     }
@@ -380,8 +384,11 @@ namespace polysat {
     void conflict::remove(signed_constraint c) {
         SASSERT(contains(c));
         m_literals.remove(c.blit().index());
-        for (pvar v : c->vars())
+        for (pvar v : c->vars()) {
             m_var_occurrences[v]--;
+            if (!m_var_occurrences[v])
+                m_vars_occurring.remove(v);
+        }
     }
 
     void conflict::remove_all() {
@@ -391,6 +398,7 @@ namespace polysat {
         m_bail_vars.reset();
         m_relevant_vars.reset();
         m_var_occurrences.reset();
+        m_vars_occurring.reset();
         m_kind = conflict_kind_t::ok;
     }
 
diff --git a/src/math/polysat/conflict.h b/src/math/polysat/conflict.h
index 0eff622d3..344796184 100644
--- a/src/math/polysat/conflict.h
+++ b/src/math/polysat/conflict.h
@@ -107,6 +107,7 @@ namespace polysat {
         uint_set m_relevant_vars;           // tracked for cone of influence but not directly involved in conflict resolution
 
         unsigned_vector m_var_occurrences;  // for each variable, the number of constraints in m_literals that contain it
+        uint_set m_vars_occurring;          // set of variables that occur in at least one of the constraints in m_literals
 
         // Additional lemmas that justify new constraints generated during conflict resolution
         clause_ref_vector m_lemmas;
@@ -177,6 +178,7 @@ namespace polysat {
         bool contains(sat::literal lit) const;
         bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
         bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
+        uint_set const& vars_occurring_in_constraints() const { return m_vars_occurring; }
 
 #if 0
         clause* side_lemma(signed_constraint c) const { SASSERT(c); return side_lemma(c.blit()); }