diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index e5fc967e5..b51862b18 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -322,6 +322,14 @@ namespace polysat {
         return any_of(c, [&](sat::literal lit) { return m_bvars.scope(lit) > 0; });        
     }
 
+    void solver::push_reinit_stack(clause& c) {
+        if (c.on_reinit_stack())
+            return;
+        c.set_on_reinit_stack(true);
+        m_clauses_to_reinit.push_back(&c);
+    }
+
+
     // TODO
     // pop_levels is called from pop and backjump
     // backjump invoked a few places.
@@ -339,6 +347,7 @@ namespace polysat {
         unsigned j = old_sz;
         for (unsigned i = old_sz; i < sz; i++) {
             clause& c = *m_clauses_to_reinit[i];
+            SASSERT(c.on_reinit_stack());
             bool reinit = false;
 #if 0
             // todo, private methods to constraint_manager
@@ -702,6 +711,7 @@ namespace polysat {
 
     void solver::push_level() {
         ++m_level;
+        m_reinit_heads.push_back(m_clauses_to_reinit.size());
         m_trail.push_back(trail_instr_t::inc_level_i);
     }
 
@@ -746,6 +756,8 @@ namespace polysat {
             case trail_instr_t::inc_level_i: {
                 --m_level;
                 --num_levels;
+                m_reinit_head = m_reinit_heads.back();
+                m_reinit_heads.pop_back();
                 break;
             }
             case trail_instr_t::viable_add_i: {
@@ -795,6 +807,9 @@ namespace polysat {
         }
         m_constraints.release_level(m_level + 1);
 
+        // todo:
+        // reinit_clauses(m_reinit_head);
+
         SASSERT(m_level == target_level);
     }
 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index e19f4e1ef..4dd49a945 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -348,6 +348,8 @@ namespace polysat {
 
         // clause reinitialization
         ptr_vector<clause>       m_clauses_to_reinit;
+        unsigned_vector          m_reinit_heads;
+        unsigned                 m_reinit_head = 0;
         void push_reinit_stack(clause& c);
         void reinit_clauses(unsigned old_sz);
         bool has_variables_to_reinit(clause const& c) const;