diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 9fee12c14..629cf266d 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -192,10 +192,9 @@ namespace polysat {
     void solver::propagate() {
         if (!can_propagate())
             return;
-        static bool propagating = false;
-        if (propagating)
+        if (m_propagating)
             return;
-        propagating = true;
+        m_propagating = true;
         push_qhead();
         while (can_propagate()) {
             auto const& item = m_search[m_qhead++];
@@ -207,6 +206,7 @@ namespace polysat {
         linear_propagate();
         SASSERT(wlist_invariant());
         SASSERT(assignment_invariant());
+        m_propagating = false;
     }
 
     /**
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index a546bca47..828833e52 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -104,8 +104,9 @@ namespace polysat {
         vector<justification>    m_justification; // justification for variable assignment
         vector<signed_constraints> m_pwatch;      // watch list datastructure into constraints.
 #ifndef NDEBUG
-        std::optional<pvar>      m_locked_wlist;  // restrict watch list modification while it is begin propagated
+        std::optional<pvar>      m_locked_wlist;  // restrict watch list modification while it is being propagated
 #endif
+        bool                     m_propagating = false;  // set to true during propagation
 
         unsigned_vector          m_activity; 
         vector<pdd>              m_vars;