diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index 1b002d604..809793d94 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -17,13 +17,14 @@ Author:
 
 namespace polysat {
 
-    sat::bool_var bool_var_manager::new_var() {
+    sat::bool_var bool_var_manager::new_var(unsigned scope) {
         sat::bool_var var;
         if (m_unused.empty()) {
             var = size();
             m_value.push_back(l_undef);
             m_value.push_back(l_undef);
             m_level.push_back(UINT_MAX);
+            m_scope.push_back(scope);
             m_deps.push_back(null_dependency);
             m_kind.push_back(kind_t::unassigned);
             m_reason.push_back(nullptr);
@@ -34,6 +35,7 @@ namespace polysat {
             var = m_unused.back();
             m_unused.pop_back();
             auto lit = sat::literal(var);
+            m_scope[var] = scope;
             SASSERT_EQ(m_value[lit.index()], l_undef);
             SASSERT_EQ(m_value[(~lit).index()], l_undef);
             SASSERT_EQ(m_level[var], UINT_MAX);
@@ -52,6 +54,7 @@ namespace polysat {
         m_value[lit.index()]    = l_undef;
         m_value[(~lit).index()] = l_undef;
         m_level[var] = UINT_MAX;
+        m_scope[var] = UINT_MAX;
         m_kind[var] = kind_t::unassigned;
         m_reason[var] = nullptr;
         m_deps[var] = null_dependency;
diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index 7b3213571..8be193f40 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -34,6 +34,7 @@ namespace polysat {
         svector<sat::bool_var>      m_unused;   // previously deleted variables that can be reused by new_var();
         svector<lbool>              m_value;    // current value (indexed by literal)
         unsigned_vector             m_level;    // level of assignment (indexed by variable)
+        unsigned_vector             m_scope;    // scope where variable is active
         dependency_vector           m_deps;     // dependencies of external asserts
         svector<kind_t>             m_kind;     // decision or propagation?
         ptr_vector<clause>          m_reason;   // reasons for bool-propagated literals
@@ -49,7 +50,7 @@ namespace polysat {
         // allocated size (not the number of active variables)
         unsigned size() const { return m_level.size(); }
 
-        sat::bool_var new_var();
+        sat::bool_var new_var(unsigned scope);
         void del_var(sat::bool_var var);
 
         bool is_assigned(sat::bool_var var) const { SASSERT(invariant(var)); return value(var) != l_undef; }
@@ -69,6 +70,9 @@ namespace polysat {
         bool is_undef(sat::literal lit) const { return value(lit) == l_undef; }
         unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; }
         unsigned level(sat::literal lit) const { return level(lit.var()); }
+        unsigned scope(sat::literal lit) const { return scope(lit.var()); }
+        unsigned scope(sat::bool_var var) const { return m_scope[var]; }
+        void set_scope(sat::bool_var var, unsigned scope) { m_scope[var] = scope; }
         clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); SASSERT(is_bool_propagation(var) == !!m_reason[var]); return m_reason[var]; }
         clause* reason(sat::literal lit) const { return reason(lit.var()); }
         dependency dep(sat::bool_var var) const { return var == sat::null_bool_var ? null_dependency : m_deps[var]; }
diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h
index af5b883d6..c1c3170bb 100644
--- a/src/math/polysat/clause.h
+++ b/src/math/polysat/clause.h
@@ -36,6 +36,7 @@ namespace polysat {
         unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
         bool m_redundant = redundant_default;
         bool m_active = false;  // clause is active iff it has been added to the solver and boolean watchlists
+        bool m_on_reinit_stack = false;
         sat::literal_vector m_literals;
         char const* m_name = "";
 
@@ -84,6 +85,9 @@ namespace polysat {
 
         void set_name(char const* name) { m_name = name; }
         char const* name() const { return m_name; }
+
+        void set_on_reinit_stack(bool f) { m_on_reinit_stack = f; }
+        bool on_reinit_stack() const { return m_on_reinit_stack; }
     };
 
     inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }
diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index a9aa194a5..46cf0738f 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -46,7 +46,7 @@ namespace polysat {
 
     void constraint_manager::ensure_bvar(constraint* c) {
         if (!c->has_bvar())
-            assign_bv2c(s.m_bvars.new_var(), c);
+            assign_bv2c(s.m_bvars.new_var(s.m_level), c);
     }
 
     void constraint_manager::erase_bvar(constraint* c) {
@@ -130,16 +130,16 @@ namespace polysat {
         SASSERT(std::all_of(cl.begin() + 1, cl.end(), [&](auto lit) { return get_watch_level(lit) <= get_watch_level(cl[1]); }));
     }
 
-    void constraint_manager::watch(clause& cl) {
+    bool constraint_manager::watch(clause& cl) {
         if (cl.empty())
-            return;
+            return false;
 
         if (cl.size() == 1) {
             if (s.m_bvars.is_false(cl[0]))
                 s.set_conflict(cl);
             else if (!s.m_bvars.is_assigned(cl[0]))
                 s.assign_propagate(cl[0], cl);
-            return;
+            return true;
         }
 
         normalize_watch(cl);
@@ -148,16 +148,17 @@ namespace polysat {
         s.m_bvars.watch(cl[1]).push_back(&cl);
 
         if (s.m_bvars.is_true(cl[0]))
-            return;
+            return false;
         SASSERT(!s.m_bvars.is_true(cl[1]));
         if (!s.m_bvars.is_false(cl[1])) {
             SASSERT(!s.m_bvars.is_assigned(cl[0]) && !s.m_bvars.is_assigned(cl[1]));
-            return;
+            return false;
         }
         if (s.m_bvars.is_false(cl[0]))
             s.set_conflict(cl);
         else
             s.assign_propagate(cl[0], cl);
+        return true;
     }
 
     void constraint_manager::unwatch(clause& cl) {
diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index d115fe72e..66a72dea9 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -77,7 +77,7 @@ namespace polysat {
         void gc_clauses();
 
         void normalize_watch(clause& cl);
-        void watch(clause& cl);
+        bool watch(clause& cl);
         void unwatch(clause& cl);
 
         void register_clause(clause* cl);
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b26718e3b..e5fc967e5 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -318,6 +318,58 @@ namespace polysat {
         }
     }
 
+    bool solver::has_variables_to_reinit(clause const& c) const {
+        return any_of(c, [&](sat::literal lit) { return m_bvars.scope(lit) > 0; });        
+    }
+
+    // TODO
+    // pop_levels is called from pop and backjump
+    // backjump invoked a few places.
+    // the logic for propagating clauses after a pop or backjump
+    // is different. pop_levels inserts into repropagate
+    // pop_levels should end with a call to reinit_clauses where
+    // old_sz is the current trail head for clauses created within the scope.
+    //
+    // pop-levels can also update the scope of variables created below the pop level.
+    // the scope of variables would be set to the new level for clauses surviving a pop.
+    
+    void solver::reinit_clauses(unsigned old_sz) {
+        unsigned sz = m_clauses_to_reinit.size();
+        SASSERT(old_sz <= sz);
+        unsigned j = old_sz;
+        for (unsigned i = old_sz; i < sz; i++) {
+            clause& c = *m_clauses_to_reinit[i];
+            bool reinit = false;
+#if 0
+            // todo, private methods to constraint_manager
+            m_constraints.unwatch(c);
+            reinit = m_constraints.watch(c);
+#endif
+
+            // reinit <- true if clause is used for propagation
+
+            // has_variables_to_reinit:
+            // = clause contains literal that was created above base level.
+            
+            // Each Boolean has a "scope". The scope is initialized to the scope where
+            // the Boolean is created.
+            
+            // TODO
+            // The scope is updated on pop to be the new level where the clause resides.
+            // the reinit-stack is also 
+
+            if (reinit && !at_base_level()) 
+                // clause propagated literal, must keep it in the reinit stack.
+                m_clauses_to_reinit[j++] = &c;            
+            else if (has_variables_to_reinit(c) && !at_base_level())
+                m_clauses_to_reinit[j++] = &c;
+            else 
+                c.set_on_reinit_stack(false);
+        }
+        m_clauses_to_reinit.shrink(j);
+    }
+
+
     bool solver::can_repropagate() {
         return !m_repropagate_lits.empty() && !is_conflict();
     }
@@ -742,6 +794,7 @@ namespace polysat {
             m_trail.pop_back();
         }
         m_constraints.release_level(m_level + 1);
+
         SASSERT(m_level == target_level);
     }
 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 4a2262d48..e19f4e1ef 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -200,6 +200,7 @@ namespace polysat {
         sat::literal_set         m_ptrue_lits;
         sat::literal_vector      m_ptrue_lits_trail;
         unsigned_vector          m_ptrue_lits_size_trail;
+        
 
         void push_qhead() {
             m_trail.push_back(trail_instr_t::qhead_i);
@@ -344,6 +345,13 @@ namespace polysat {
 
         signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
 
+
+        // clause reinitialization
+        ptr_vector<clause>       m_clauses_to_reinit;
+        void push_reinit_stack(clause& c);
+        void reinit_clauses(unsigned old_sz);
+        bool has_variables_to_reinit(clause const& c) const;
+
         bool inc() { return m_lim.inc(); }
 
         void log_lemma_smt2(clause& clause);