diff --git a/src/math/polysat/log.h b/src/math/polysat/log.h
index acabfb53d..1d2e02d5b 100644
--- a/src/math/polysat/log.h
+++ b/src/math/polysat/log.h
@@ -76,6 +76,7 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
 #define LOG(x)    LOG_(LogLevel::Default , x)
 #define LOG_V(x)  LOG_(LogLevel::Verbose , x)
 #define COND_LOG(c, x) if (c) LOG(x)
+#define LOGE(x)   LOG(#x << " = " << (x))
 
 #define IF_LOGGING(x) \
   do {                \
@@ -96,6 +97,8 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
 #define LOG_H3(x) LOG_(0, x)
 #define LOG(x)    LOG_(0, x)
 #define LOG_V(x)  LOG_(0, x)
+#define COND_LOG(c, x)  LOG_(c, x)
+#define LOGE(x)   LOG_(0, x)
 
 #define IF_LOGGING(x) \
   do {                \
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 35dbb2a26..9fee12c14 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -192,6 +192,10 @@ namespace polysat {
     void solver::propagate() {
         if (!can_propagate())
             return;
+        static bool propagating = false;
+        if (propagating)
+            return;
+        propagating = true;
         push_qhead();
         while (can_propagate()) {
             auto const& item = m_search[m_qhead++];
@@ -230,14 +234,19 @@ namespace polysat {
     */
     void solver::propagate(pvar v) {
         LOG_H2("Propagate v" << v);
+        SASSERT(!m_locked_wlist);
+        DEBUG_CODE(m_locked_wlist = v;);
         auto& wlist = m_pwatch[v];
         unsigned i = 0, j = 0, sz = wlist.size();
+        LOG("wlist old: " << wlist);
         for (; i < sz && !is_conflict(); ++i)
             if (!wlist[i].propagate(*this, v))
                 wlist[j++] = wlist[i];
         for (; i < sz; ++i)
             wlist[j++] = wlist[i];
         wlist.shrink(j);
+        LOG("wlist new: " << wlist);
+        DEBUG_CODE(m_locked_wlist = std::nullopt;);
     }
 
     bool solver::propagate(sat::literal lit, clause& cl) {
@@ -374,6 +383,7 @@ namespace polysat {
 
     void solver::add_watch(signed_constraint c, pvar v) {
         SASSERT(c);
+        // SASSERT(m_locked_wlist != v);  // appending doesn't interfere with propagation, so it should be fine
         LOG("Watching v" << v << " in constraint " << c);
         m_pwatch[v].push_back(c);
     }
@@ -389,6 +399,7 @@ namespace polysat {
     void solver::erase_watch(pvar v, signed_constraint c) {
         if (v == null_var)
             return;
+        SASSERT(m_locked_wlist != v);
         auto& wlist = m_pwatch[v];
         unsigned sz = wlist.size();
         for (unsigned i = 0; i < sz; ++i) {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 47012dd2a..a546bca47 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -103,6 +103,9 @@ namespace polysat {
         vector<rational>         m_value;         // assigned value
         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
+#endif
 
         unsigned_vector          m_activity; 
         vector<pdd>              m_vars;