diff --git a/src/sat/sat_gc.cpp b/src/sat/sat_gc.cpp
index 96d0f495ac0..2179a324fe7 100644
--- a/src/sat/sat_gc.cpp
+++ b/src/sat/sat_gc.cpp
@@ -423,6 +423,64 @@ namespace sat {
         return true;
     }
 
+    void solver::gc_vars(bool_var max_var) {
+        init_visited();
+        m_aux_literals.reset();
+        auto gc_watch = [&](literal lit) {
+            auto& wl1 = get_wlist(lit);
+            for (auto w : get_wlist(lit)) {
+                if (w.is_binary_clause() && w.get_literal().var() < max_var && !is_visited(w.get_literal())) {
+                    m_aux_literals.push_back(w.get_literal());
+                    mark_visited(w.get_literal());
+                }
+            }
+            wl1.reset();
+        };
+        for (unsigned v = max_var; v < num_vars(); ++v) {
+            gc_watch(literal(v, false));
+            gc_watch(literal(v, true));
+        }
+
+        for (literal lit : m_aux_literals) {
+            auto& wl2 = get_wlist(~lit);
+            unsigned j = 0;
+            for (auto w2 : wl2) 
+                if (!w2.is_binary_clause() || w2.get_literal().var() < max_var)
+                    wl2[j++] = w2;
+            wl2.shrink(j);                        
+        }
+        m_aux_literals.reset();
+
+        auto gc_clauses = [&](ptr_vector<clause>& clauses) {
+            unsigned j = 0;
+            for (clause* c : clauses) {
+                bool should_remove = false;
+                for (auto lit : *c) 
+                    should_remove |= lit.var() >= max_var;
+                if (should_remove) {
+                    SASSERT(!c->on_reinit_stack());
+                    detach_clause(*c);
+                    del_clause(*c);
+                }
+                else {
+                    clauses[j++] = c;
+                }
+            }
+            clauses.shrink(j);
+        };
+        gc_clauses(m_learned);
+        gc_clauses(m_clauses);
+        
+        unsigned j = 0;
+        for (literal lit : m_trail) {
+            SASSERT(lvl(lit) == 0);
+            if (lit.var() < max_var)
+                m_trail[j++] = lit;
+        }
+        m_trail.shrink(j);
+        shrink_vars(max_var);
+    }
+
 #if 0
     void solver::gc_reinit_stack(unsigned num_scopes) {
         SASSERT (!at_base_lvl());
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index a280ee94d10..ba1309d0cc2 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -558,22 +558,27 @@ namespace sat {
         m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
         m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
         m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
-        if (!at_base_lvl()) {
-            if (value(c[1]) == l_false && value(c[2]) == l_false) {
-                m_stats.m_ter_propagate++;
-                assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2]));
-                reinit = !c.is_learned();
-            }
-            else if (value(c[0]) == l_false && value(c[2]) == l_false) {
-                m_stats.m_ter_propagate++;
-                assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2]));
-                reinit = !c.is_learned();
-            }
-            else if (value(c[0]) == l_false && value(c[1]) == l_false) {
-                m_stats.m_ter_propagate++;
-                assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1]));
-                reinit = !c.is_learned();
-            }
+        if (!at_base_lvl()) 
+            reinit = propagate_ter_clause(c);        
+        return reinit;
+    }
+
+    bool solver::propagate_ter_clause(clause& c) {
+        bool reinit = false;
+        if (value(c[1]) == l_false && value(c[2]) == l_false) {
+            m_stats.m_ter_propagate++;
+            assign(c[0], justification(std::max(lvl(c[1]), lvl(c[2])), c[1], c[2]));
+            reinit = !c.is_learned();
+        }
+        else if (value(c[0]) == l_false && value(c[2]) == l_false) {
+            m_stats.m_ter_propagate++;
+            assign(c[1], justification(std::max(lvl(c[0]), lvl(c[2])), c[0], c[2]));
+            reinit = !c.is_learned();
+        }
+        else if (value(c[0]) == l_false && value(c[1]) == l_false) {
+            m_stats.m_ter_propagate++;
+            assign(c[2], justification(std::max(lvl(c[0]), lvl(c[1])), c[0], c[1]));
+            reinit = !c.is_learned();
         }
         return reinit;
     }
@@ -3459,8 +3464,8 @@ namespace sat {
     }
 
     void solver::pop_vars(unsigned num_scopes) {
-        integrity_checker check(*this);
-        check.check_reinit_stack();
+        //integrity_checker check(*this);
+        //check.check_reinit_stack();
         m_vars_to_reinit.reset();
         unsigned old_num_vars = m_vars_lim.pop(num_scopes);
         if (old_num_vars == m_active_vars.size())
@@ -3471,7 +3476,7 @@ namespace sat {
 
         gc_reinit_stack(num_scopes);        
 
-        check.check_reinit_stack();
+        // check.check_reinit_stack();
         init_visited();
         unsigned old_sz = m_scopes[new_lvl].m_clauses_to_reinit_lim;
         for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; ) {
@@ -3575,9 +3580,8 @@ namespace sat {
         SASSERT(old_sz <= m_trail.size());
         SASSERT(m_replay_assign.empty());
         unsigned i = m_trail.size();
-        while (i != old_sz) {
-            --i;
-            literal l                  = m_trail[i];
+        for (unsigned i = m_trail.size(); i-- > old_sz; ) {
+            literal l  = m_trail[i];
             bool_var v = l.var();
             if (lvl(v) <= new_lvl) {
                 m_replay_assign.push_back(l);
@@ -3618,6 +3622,15 @@ namespace sat {
             }
             else {
                 clause & c = *(cw.get_clause());
+                if (ENABLE_TERNARY && c.size() == 3) {
+                    if (!at_base_lvl() && propagate_ter_clause(c))
+                        m_clauses_to_reinit[j++] = cw;                
+                    else if (has_variables_to_reinit(c))
+                        m_clauses_to_reinit[j++] = cw;
+                    else 
+                        c.set_reinit_stack(false);
+                    continue;
+                }
                 detach_clause(c);
                 attach_clause(c, reinit);
                 if (!at_base_lvl() && reinit) 
@@ -3639,9 +3652,10 @@ namespace sat {
 
     void solver::user_push() {
         pop_to_base_level();
-        literal lit;
+        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);
-        lit = literal(new_v, false);
+        literal lit = literal(new_v, false);
         m_user_scope_literals.push_back(lit);
         m_cut_simplifier = nullptr; // for simplicity, wipe it out
         if (m_ext)
@@ -3649,108 +3663,26 @@ namespace sat {
         TRACE("sat", tout << "user_push: " << lit << "\n";);
     }
 
-    void solver::gc_lit(clause_vector &clauses, literal lit) {
-        unsigned j = 0;
-        for (unsigned i = 0; i < clauses.size(); ++i) {
-            clause & c = *(clauses[i]);
-            if (c.contains(lit) || c.contains(~lit)) {
-                detach_clause(c);
-                del_clause(c);
-            }
-            else {
-                clauses[j] = &c;
-                ++j;
-            }
-        }
-        clauses.shrink(j);
-    }
-
-    void solver::gc_bin(literal lit) {
-        bool_var v = lit.var();
-        for (watch_list& wlist : m_watches) {
-            watch_list::iterator it  = wlist.begin();
-            watch_list::iterator it2 = wlist.begin();
-            watch_list::iterator end = wlist.end();
-            for (; it != end; ++it) {
-                if (it->is_binary_clause() && it->get_literal().var() == v) {
-                    // skip
-                }
-                else {
-                    *it2 = *it;
-                    ++it2;
-                }
-            }
-            wlist.set_end(it2);
-        }
-    }
-
-    bool_var solver::max_var(bool redundant, bool_var v) {
-        m_user_bin_clauses.reset();
-        collect_bin_clauses(m_user_bin_clauses, redundant, false);
-        for (unsigned i = 0; i < m_user_bin_clauses.size(); ++i) {
-            literal l1 = m_user_bin_clauses[i].first;
-            literal l2 = m_user_bin_clauses[i].second;
-            if (l1.var() > v) v = l1.var();
-            if (l2.var() > v) v = l2.var();
-        }
-        return v;
-    }
-
-    bool_var solver::max_var(clause_vector& clauses, bool_var v) {
-        for (clause* cp : clauses) 
-            for (auto it = cp->begin(), end = cp->end(); it != end; ++it) {
-                if (it->var() > v) 
-                    v = it->var();
-            }
-        return v;
-    }
-
-    void solver::gc_var(bool_var v) {
-        bool_var w = max_var(m_learned, v);
-        w = max_var(m_clauses, w);
-        w = max_var(true, w);
-        w = max_var(false, w);
-        v = m_mc.max_var(w);
-        for (literal lit : m_trail) {
-            w = std::max(w, lit.var());
-        }
-        if (m_ext) {
-            w = m_ext->max_var(w);
-        }
-        v = w + 1;
-        
-        // v is an index of a variable that does not occur in solver state.
-        if (v < m_justification.size()) {
-            shrink_vars(v);
-        }
-    }
-
     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();
+        m_user_scope_literals.shrink(old_sz);
+
         pop_to_base_level();
-        TRACE("sat", display(tout););
         if (m_ext)
             m_ext->user_pop(num_scopes);
-        while (num_scopes > 0) {
-            literal lit = m_user_scope_literals.back();
-            m_user_scope_literals.pop_back();
-            get_wlist(lit).reset();
-            get_wlist(~lit).reset();
-
-            gc_lit(m_learned, lit);
-            gc_lit(m_clauses, lit);
-            gc_bin(lit);
-            TRACE("sat", tout << "gc: " << lit << "\n"; display(tout););
-            --num_scopes;
-            for (unsigned i = 0; i < m_trail.size(); ++i) {
-                if (m_trail[i] == lit) {
-                    TRACE("sat", tout << m_trail << "\n";);
-                    unassign_vars(i, 0);
-                    break;
-                }
-            }
-            gc_var(lit.var());            
-        }
+
+        gc_vars(max_var);
+        TRACE("sat", display(tout););
+
         m_qhead = 0;
+        unsigned j = 0;
+        for (bool_var v : m_free_vars) 
+            if (v < max_var)
+                m_free_vars[j++] = v;
+        m_free_vars.shrink(j);
+        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);
     }
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 5ada5ef88cd..6725057c312 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -287,6 +287,7 @@ namespace sat {
         bool propagate_bin_clause(literal l1, literal l2);
         clause * mk_ter_clause(literal * lits, status st);
         bool attach_ter_clause(clause & c, status st);
+        bool propagate_ter_clause(clause& c);
         clause * mk_nary_clause(unsigned num_lits, literal * lits, status st);
         bool has_variables_to_reinit(clause const& c) const;
         bool has_variables_to_reinit(literal l1, literal l2) const;
@@ -651,14 +652,11 @@ namespace sat {
         void reinit_clauses(unsigned old_sz);
 
         literal_vector m_user_scope_literals;
+        vector<svector<bool_var>> m_free_var_freeze;
         literal_vector m_aux_literals;
         svector<bin_clause> m_user_bin_clauses;
-        void gc_lit(clause_vector& clauses, literal lit);
-        void gc_bin(literal lit);
-        void gc_var(bool_var v);
 
-        bool_var max_var(clause_vector& clauses, bool_var v);
-        bool_var max_var(bool learned, bool_var v);
+        void gc_vars(bool_var max_var);
 
         // -----------------------
         //