diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 6a5f15567..7370ed266 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -428,9 +428,8 @@ namespace sat {
             }
 
             ++m_stats.m_non_learned_generation;
-            if (!m_searching) {
-                m_mc.add_clause(num_lits, lits);
-            }
+            if (!m_searching) 
+                m_mc.add_clause(num_lits, lits);            
         }       
 
 
@@ -945,6 +944,7 @@ namespace sat {
 
     void solver::assign_core(literal l, justification j) {
         SASSERT(value(l) == l_undef);
+        SASSERT(!m_trail.contains(l) && !m_trail.contains(~l));
         TRACE("sat_assign_core", tout << l << " " << j << "\n";);
         if (j.level() == 0) {
             if (m_config.m_drat) 
@@ -3654,11 +3654,14 @@ namespace sat {
             }
         }
         m_trail.shrink(old_sz);        
+        DEBUG_CODE(for (literal l : m_trail) SASSERT(lvl(l.var()) <= new_lvl););
         m_qhead = m_trail.size();
         if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n");
         CTRACE("sat", !m_replay_assign.empty(), tout << "replay-assign: " << m_replay_assign << "\n";);
         for (unsigned i = m_replay_assign.size(); i-- > 0; ) {
             literal lit = m_replay_assign[i];
+            SASSERT(value(lit) == l_true);
+            SASSERT(!m_trail.contains(lit) && !m_trail.contains(~lit));
             m_trail.push_back(lit);            
         }
         
@@ -3709,11 +3712,11 @@ namespace sat {
     //
 
     void solver::user_push() {
-
         pop_to_base_level();
         m_free_var_freeze.push_back(m_free_vars);
         m_free_vars.reset(); // resetting free_vars forces new variables to be assigned above new_v
         bool_var new_v = mk_var(true, false);
+        SASSERT(new_v + 1 == m_justification.size()); // there are no active variables that have higher values
         literal lit = literal(new_v, false);
         m_user_scope_literals.push_back(lit);
         m_cut_simplifier = nullptr; // for simplicity, wipe it out
@@ -3724,13 +3727,13 @@ namespace sat {
 
     void solver::user_pop(unsigned num_scopes) {
         unsigned old_sz = m_user_scope_literals.size() - num_scopes;
-        bool_var max_var = m_user_scope_literals[old_sz].var();
+        bool_var max_var = m_user_scope_literals[old_sz].var();        
         m_user_scope_literals.shrink(old_sz);
 
         pop_to_base_level();
         if (m_ext)
             m_ext->user_pop(num_scopes);
-
+    
         gc_vars(max_var);
         TRACE("sat", display(tout););
 
@@ -3743,7 +3746,7 @@ namespace sat {
         m_free_vars.append(m_free_var_freeze[old_sz]); 
         m_free_var_freeze.shrink(old_sz);
         scoped_suspend_rlimit _sp(m_rlimit);
-        propagate(false);
+        propagate(false);     
     }
 
     void solver::pop_to_base_level() {
@@ -4832,20 +4835,22 @@ namespace sat {
         return true;
     }
 
+    void solver::init_ts(unsigned n, svector<unsigned>& v, unsigned& ts) {
+        if (v.empty()) 
+            ts = 0;
+        
+        ts++;
+        if (ts == 0) {
+            ts = 1;
+            v.reset();
+        }
+        while (v.size() < n) 
+            v.push_back(0);        
+    }
+
     void solver::init_visited() {
-        if (m_visited.empty()) {
-            m_visited_ts = 0;
-        }
-        m_visited_ts++;
-        if (m_visited_ts == 0) {
-            m_visited_ts = 1;
-            m_visited.reset();
-        }
-        while (m_visited.size() < 2*num_vars()) {
-            m_visited.push_back(0);
-        }
+        init_ts(2 * num_vars(), m_visited, m_visited_ts);
     }
 
 
-
 };
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 3228bcf60..0b01b777c 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -343,6 +343,7 @@ namespace sat {
         void push_reinit_stack(clause & c);
         void push_reinit_stack(literal l1, literal l2);
 
+        void init_ts(unsigned n, svector<unsigned>& v, unsigned& ts);
         void init_visited();
         void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; }
         void mark_visited(bool_var v) { mark_visited(literal(v, false)); }