From b968898b7e7361a54c279f081c54caef3dc239cb Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 20 Jan 2022 17:09:36 +0100
Subject: [PATCH] use member variable rather that static

---
 src/math/polysat/solver.cpp | 6 +++---
 src/math/polysat/solver.h   | 3 ++-
 2 files changed, 5 insertions(+), 4 deletions(-)

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;