diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index 0d0c148f1..71980eeab 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -202,8 +202,7 @@ namespace sat {
             for (unsigned i = 0; i < p.size(); ++i) {
                 wlits.push_back(p[i]);
             }
-            bool_var v = p.lit() == null_literal ? null_bool_var : p.lit().var();
-            result.add_pb_ge(v, wlits, p.k());
+            result.add_pb_ge(p.lit(), wlits, p.k());
         }
     }
 
@@ -439,21 +438,18 @@ namespace sat {
     }
 
     void card_extension::display(std::ostream& out, pb const& p, bool values) const {
-        if (p.lit() != null_literal) out << p.lit();
-        out << "[watch: " << p.num_watch() << ", slack: " << p.slack() << "]";
+        if (p.lit() != null_literal) out << p.lit() << " == ";
         if (p.lit() != null_literal && values) {
+            out << "[watch: " << p.num_watch() << ", slack: " << p.slack() << "]";
             out << "@(" << value(p.lit());
             if (value(p.lit()) != l_undef) {
                 out << ":" << lvl(p.lit());
             }
             out << "): ";
         }
-        else {
-            out << ": ";
-        }
-        for (unsigned i = 0; i < p.size(); ++i) {
-            literal l = p[i].second;
-            unsigned w = p[i].first;
+        for (wliteral wl : p) {
+            literal l = wl.second;
+            unsigned w = wl.first;
             if (w > 1) out << w << " * ";
             out << l;
             if (values) {
@@ -476,11 +472,10 @@ namespace sat {
         for (unsigned i = 0; i < m_xors.size(); ++i) {
             literal_vector lits;
             xor& x = *m_xors[i];
-            for (unsigned i = 0; i < x.size(); ++i) {
-                lits.push_back(x[i]);
+            for (literal l : x) {
+                lits.push_back(l);
             }
-            bool_var v = x.lit() == null_literal ? null_bool_var : x.lit().var();
-            result.add_xor(v, lits);
+            result.add_xor(x.lit(), lits);
         }
     }
 
@@ -1011,53 +1006,63 @@ namespace sat {
         m_stats.reset();
     }
 
-    void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
+    void card_extension::add_at_least(literal lit, literal_vector const& lits, unsigned k) {
         unsigned index = 4*m_cards.size();
         SASSERT(is_card_index(index));
-        literal lit = v == null_bool_var ? null_literal : literal(v, false);
         card* c = new (memory::allocate(card::get_obj_size(lits.size()))) card(index, lit, lits, k);
         m_cards.push_back(c);
-        if (v == null_bool_var) {
+        if (lit == null_literal) {
             // it is an axiom.
             init_watch(*c, true);
             m_card_axioms.push_back(c);
         }
         else {
-            get_wlist(literal(v, false)).push_back(index);
-            get_wlist(literal(v, true)).push_back(index);
+            get_wlist(lit).push_back(index);
+            get_wlist(~lit).push_back(index);
+            m_index_trail.push_back(index);
+        }
+    }
+
+    void card_extension::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
+        literal lit = v == null_bool_var ? null_literal : literal(v, false);
+        add_at_least(lit, lits, k);
+    }
+
+    void card_extension::add_pb_ge(literal lit, svector<wliteral> const& wlits, unsigned k) {
+        unsigned index = 4*m_pbs.size() + 0x3;
+        SASSERT(is_pb_index(index));
+        pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
+        m_pbs.push_back(p);
+        if (lit == null_literal) {
+            init_watch(*p, true);
+            m_pb_axioms.push_back(p);
+        }
+        else {
+            get_wlist(lit).push_back(index);
+            get_wlist(~lit).push_back(index);
             m_index_trail.push_back(index);
         }
     }
 
     void card_extension::add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k) {
-        unsigned index = 4*m_pbs.size() + 0x3;
-        SASSERT(is_pb_index(index));
         literal lit = v == null_bool_var ? null_literal : literal(v, false);
-        pb* p = new (memory::allocate(pb::get_obj_size(wlits.size()))) pb(index, lit, wlits, k);
-        m_pbs.push_back(p);
-        if (v == null_bool_var) {
-            init_watch(*p, true);
-            m_pb_axioms.push_back(p);
-        }
-        else {
-            get_wlist(literal(v, false)).push_back(index);
-            get_wlist(literal(v, true)).push_back(index);
-            m_index_trail.push_back(index);
-        }
+        add_pb_ge(lit, wlits, k);
     }
 
 
     void card_extension::add_xor(bool_var v, literal_vector const& lits) {
-        unsigned index = 4*m_xors.size() + 0x1;
-        SASSERT(is_xor_index(index));
-        SASSERT(v != null_bool_var);
-        xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, literal(v, false), lits);
-        m_xors.push_back(x);
-        get_wlist(literal(v, false)).push_back(index);
-        get_wlist(literal(v, true)).push_back(index);
-        m_index_trail.push_back(index);
+        add_xor(literal(v, false), lits);
     }
 
+    void card_extension::add_xor(literal lit, literal_vector const& lits) {
+        unsigned index = 4*m_xors.size() + 0x1;
+        SASSERT(is_xor_index(index));
+        xor* x = new (memory::allocate(xor::get_obj_size(lits.size()))) xor(index, lit, lits);
+        m_xors.push_back(x);
+        get_wlist(lit).push_back(index);
+        get_wlist(~lit).push_back(index);
+        m_index_trail.push_back(index);
+    }
 
     void card_extension::propagate(literal l, ext_constraint_idx idx, bool & keep) {
         SASSERT(value(l) == l_true);
@@ -1412,18 +1417,20 @@ namespace sat {
     void card_extension::clauses_modifed() {}
     lbool card_extension::get_phase(bool_var v) { return l_undef; }
 
-    extension* card_extension::copy(solver* s) {
-        card_extension* result = alloc(card_extension);
-        result->set_solver(s);
+    void card_extension::copy_card(card_extension& result) {
         for (unsigned i = 0; i < m_cards.size(); ++i) {
             literal_vector lits;
             card& c = *m_cards[i];
             for (unsigned i = 0; i < c.size(); ++i) {
                 lits.push_back(c[i]);
             }
-            bool_var v = c.lit() == null_literal ? null_bool_var : c.lit().var();
-            result->add_at_least(v, lits, c.k());
+            result.add_at_least(c.lit(), lits, c.k());
         }
+    }
+    extension* card_extension::copy(solver* s) {
+        card_extension* result = alloc(card_extension);
+        result->set_solver(s);
+        copy_card(*result);
         copy_xor(*result);
         copy_pb(*result);
         return result;
@@ -1498,16 +1505,18 @@ namespace sat {
     }
 
     void card_extension::display(std::ostream& out, card const& c, bool values) const {
-        out << c.lit() << "[" << c.size() << "]";
-        if (c.lit() != null_literal && values) {
-            out << "@(" << value(c.lit());
-            if (value(c.lit()) != l_undef) {
-                out << ":" << lvl(c.lit());
+        if (c.lit() != null_literal) {
+            if (values) {
+                out << c.lit() << "[" << c.size() << "]";
+                out << "@(" << value(c.lit());
+                if (value(c.lit()) != l_undef) {
+                    out << ":" << lvl(c.lit());
+                }
+                out << "): ";
+            }
+            else {
+                out << c.lit() << " == ";
             }
-            out << "): ";
-        }
-        else {
-            out << ": ";
         }
         for (unsigned i = 0; i < c.size(); ++i) {
             literal l = c[i];
@@ -1527,6 +1536,15 @@ namespace sat {
     }
 
     std::ostream& card_extension::display(std::ostream& out) const {
+        for (card* c : m_cards) {
+            display(out, *c, false);
+        }
+        for (pb* p : m_pbs) {
+            display(out, *p, false);
+        }
+        for (xor* x : m_xors) {
+            display(out, *x, false);
+        }
         return out;
     }
 
diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h
index 3b9bfd5c0..37b368e70 100644
--- a/src/sat/card_extension.h
+++ b/src/sat/card_extension.h
@@ -108,6 +108,8 @@ namespace sat {
             literal lit() const { return m_lit; }
             literal operator[](unsigned i) const { return m_lits[i]; }
             unsigned size() const { return m_size; }
+            literal const* begin() const { return m_lits; }
+            literal const* end() const { return (literal const*)m_lits + m_size; }
             void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
             void negate() { m_lits[0].neg(); }
         };
@@ -167,7 +169,7 @@ namespace sat {
         void reset_marked_literals();
         void unwatch_literal(literal w, card& c);
         void get_card_antecedents(literal l, card const& c, literal_vector & r);
-
+        void copy_card(card_extension& result);
 
         // xor specific functionality
         void copy_xor(card_extension& result);
@@ -244,6 +246,10 @@ namespace sat {
         void display(std::ostream& out, pb const& p, bool values) const;
         void display(std::ostream& out, xor const& c, bool values) const;
 
+        void add_at_least(literal l, literal_vector const& lits, unsigned k);
+        void add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k);
+        void add_xor(literal l, literal_vector const& lits);
+
     public:
         card_extension();
         virtual ~card_extension();
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 5e218f278..b53b920dd 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1102,11 +1102,9 @@ namespace sat {
 
     unsigned simplifier::get_num_non_learned_bin(literal l) const {
         unsigned r = 0;
-        watch_list const & wlist  = get_wlist(~l);
-        watch_list::const_iterator it  = wlist.begin();
-        watch_list::const_iterator end = wlist.end();
-        for (; it != end; ++it) {
-            if (it->is_binary_non_learned_clause())
+        watch_list const & wlist = get_wlist(~l);
+        for (auto & w : wlist) {
+            if (w.is_binary_non_learned_clause())
                 r++;
         }
         return r;
@@ -1133,10 +1131,7 @@ namespace sat {
 
     void simplifier::order_vars_for_elim(bool_var_vector & r) {
         svector<bool_var_and_cost> tmp;
-        bool_var_set::iterator it  = m_elim_todo.begin();
-        bool_var_set::iterator end = m_elim_todo.end();
-        for (; it != end; ++it) {
-            bool_var v = *it;
+        for (bool_var v : m_elim_todo) {
             if (is_external(v))
                 continue;
             if (was_eliminated(v))
@@ -1149,17 +1144,10 @@ namespace sat {
         m_elim_todo.reset();
         std::stable_sort(tmp.begin(), tmp.end(), bool_var_and_cost_lt());
         TRACE("elim_vars",
-              svector<bool_var_and_cost>::iterator it  = tmp.begin();
-              svector<bool_var_and_cost>::iterator end = tmp.end();
-              for (; it != end; ++it) {
-                  tout << "(" << it->first << ", " << it->second << ") ";
-              }
+              for (auto& p : tmp) tout << "(" << p.first << ", " << p.second << ") ";
               tout << "\n";);
-        svector<bool_var_and_cost>::iterator it2  = tmp.begin();
-        svector<bool_var_and_cost>::iterator end2 = tmp.end();
-        for (; it2 != end2; ++it2) {
-            r.push_back(it2->first);
-        }
+        for (auto& p : tmp) 
+            r.push_back(p.first);
     }
 
     /**
@@ -1175,11 +1163,9 @@ namespace sat {
         }
 
         watch_list & wlist = get_wlist(~l);
-        watch_list::iterator it2  = wlist.begin();
-        watch_list::iterator end2 = wlist.end();
-        for (; it2 != end2; ++it2) {
-            if (it2->is_binary_non_learned_clause()) {
-                r.push_back(clause_wrapper(l, it2->get_literal()));
+        for (auto & w : wlist) {
+            if (w.is_binary_non_learned_clause()) {
+                r.push_back(clause_wrapper(l, w.get_literal()));
                 SASSERT(r.back().size() == 2);
             }
         }
@@ -1199,7 +1185,7 @@ namespace sat {
         bool res = true;
         unsigned sz = c1.size();
         m_elim_counter -= sz;
-        for (unsigned i = 0; i < sz; i++) {
+        for (unsigned i = 0; i < sz; ++i) {
             literal l2 = c1[i];
             if (l == l2)
                 continue;
@@ -1210,7 +1196,7 @@ namespace sat {
         literal not_l = ~l;
         sz = c2.size();
         m_elim_counter -= sz;
-        for (unsigned i = 0; i < sz; i++) {
+        for (unsigned i = 0; i < sz; ++i) {
             literal l2 = c2[i];
             if (not_l == l2)
                 continue;
@@ -1223,7 +1209,7 @@ namespace sat {
         }
 
         sz = c1.size();
-        for (unsigned i = 0; i < sz; i++) {
+        for (unsigned i = 0; i < sz; ++i) {
             literal l2 = c1[i];
             if (l == l2)
                 continue;
@@ -1234,10 +1220,9 @@ namespace sat {
 
     void simplifier::save_clauses(model_converter::entry & mc_entry, clause_wrapper_vector const & cs) {
         model_converter & mc = s.m_mc;
-        clause_wrapper_vector::const_iterator it  = cs.begin();
-        clause_wrapper_vector::const_iterator end = cs.end();
-        for (; it != end; ++it)
-            mc.insert(mc_entry, *it);
+        for (auto & e : cs) {
+            mc.insert(mc_entry, e);
+        }
     }
 
     void simplifier::add_non_learned_binary_clause(literal l1, literal l2) {
@@ -1273,11 +1258,9 @@ namespace sat {
     */
     void simplifier::remove_bin_clauses(literal l) {
         watch_list & wlist = get_wlist(~l);
-        watch_list::iterator it  = wlist.begin();
-        watch_list::iterator end = wlist.end();
-        for (; it != end; ++it) {
-            if (it->is_binary_clause()) {
-                literal l2 = it->get_literal();
+        for (auto & w : wlist) {
+            if (w.is_binary_clause()) {
+                literal l2 = w.get_literal();
                 watch_list & wlist2 = get_wlist(~l2);
                 watch_list::iterator it2  = wlist2.begin();
                 watch_list::iterator itprev = it2;
@@ -1292,7 +1275,7 @@ namespace sat {
                     itprev++;
                 }
                 wlist2.set_end(itprev);
-                m_sub_bin_todo.erase(bin_clause(l, l2, it->is_learned()));
+                m_sub_bin_todo.erase(bin_clause(l, l2, w.is_learned()));
             }
         }
         TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";);
@@ -1484,13 +1467,10 @@ namespace sat {
         bool_var_vector vars;
         order_vars_for_elim(vars);
 
-        bool_var_vector::iterator it  = vars.begin();
-        bool_var_vector::iterator end = vars.end();
-        for (; it != end; ++it) {
+        for (bool_var v : vars) {
             checkpoint();
             if (m_elim_counter < 0)
                 return;
-            bool_var v = *it;
             if (try_eliminate(v)) {
                 m_num_elim_vars++;
             }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 93021a16e..405b44b21 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -96,6 +96,9 @@ namespace sat {
                 if (src.was_eliminated(v)) {
                     m_eliminated[v] = true;
                 }
+                m_phase[v] = src.m_phase[v];
+                m_prev_phase[v] = src.m_prev_phase[v];
+                // m_activity[v] = src.m_activity[v], but then update case_split_queue ? 
             }
         }
 
@@ -117,14 +120,14 @@ namespace sat {
             unsigned sz = src.m_watches.size();
             for (unsigned l_idx = 0; l_idx < sz; ++l_idx) {
                 literal l = ~to_literal(l_idx);
+                if (src.was_eliminated(l.var())) continue;
                 watch_list const & wlist = src.m_watches[l_idx];
-                watch_list::const_iterator it  = wlist.begin();
-                watch_list::const_iterator end = wlist.end();
-                for (; it != end; ++it) {
-                    if (!it->is_binary_non_learned_clause())
+                for (auto & wi : wlist) {
+                    if (!wi.is_binary_non_learned_clause())
                         continue;
-                    literal l2 = it->get_literal();
-                    if (l.index() > l2.index())
+                    literal l2 = wi.get_literal();
+                    if (l.index() > l2.index() ||
+                        src.was_eliminated(l2.var()))
                         continue;
                     mk_clause_core(l, l2);
                 }
@@ -133,16 +136,24 @@ namespace sat {
 
         {
             literal_vector buffer;
-            // copy clause
-            clause_vector::const_iterator it  = src.m_clauses.begin();
-            clause_vector::const_iterator end = src.m_clauses.end();
-            for (; it != end; ++it) {
-                clause const & c = *(*it);
+            // copy clauses
+            for (clause* c : src.m_clauses) {
                 buffer.reset();
-                for (unsigned i = 0; i < c.size(); i++)
-                    buffer.push_back(c[i]);
+                for (literal l : *c) buffer.push_back(l);
                 mk_clause_core(buffer);
             }
+            // copy high quality lemmas
+            for (clause* c : src.m_learned) {
+                if (c->glue() <= 2 || (c->size() <= 40 && c->glue() <= 8)) {
+                    buffer.reset();
+                    for (literal l : *c) buffer.push_back(l);
+                    clause* c1 = mk_clause_core(buffer.size(), buffer.c_ptr(), true);
+                    if (c1) {
+                        c1->set_glue(c->glue());
+                        c1->set_psm(c->psm());
+                    }
+                }
+            }
         }
 
         m_user_scope_literals.reset();
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 6e124fcf3..295a04a67 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -45,7 +45,6 @@ class inc_sat_solver : public solver {
     sat::solver     m_solver;
     goal2sat        m_goal2sat;
     params_ref      m_params;
-    bool            m_optimize_model; // parameter
     expr_ref_vector m_fmls;
     expr_ref_vector m_asmsf;
     unsigned_vector m_fmls_lim;
@@ -77,7 +76,7 @@ public:
     inc_sat_solver(ast_manager& m, params_ref const& p):
         m(m), 
         m_solver(p, m.limit()),
-        m_params(p), m_optimize_model(false),
+        m_params(p), 
         m_fmls(m),
         m_asmsf(m),
         m_fmls_head(0),
@@ -96,20 +95,24 @@ public:
     virtual ~inc_sat_solver() {}
 
     virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
-        ast_translation tr(m, dst_m);
         if (m_num_scopes > 0) {
             throw default_exception("Cannot translate sat solver at non-base level");
         }
+        ast_translation tr(m, dst_m);
+        m_solver.pop_to_base_level();
         inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p);
-        expr_ref fml(dst_m);
-        for (unsigned i = 0; i < m_fmls.size(); ++i) {
-            fml = tr(m_fmls[i].get());
-            result->m_fmls.push_back(fml);
-        }
-        for (unsigned i = 0; i < m_asmsf.size(); ++i) {
-            fml = tr(m_asmsf[i].get());
-            result->m_asmsf.push_back(fml);
-        }
+        result->m_solver.copy(m_solver);
+        result->m_fmls_head = m_fmls_head;
+        for (expr* f : m_fmls) result->m_fmls.push_back(tr(f));
+        for (expr* f : m_asmsf) result->m_asmsf.push_back(tr(f));
+        for (auto & kv : m_map) result->m_map.insert(tr(kv.m_key), kv.m_value);
+        for (unsigned l : m_fmls_lim) result->m_fmls_lim.push_back(l);
+        for (unsigned a : m_asms_lim) result->m_asms_lim.push_back(a);
+        for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h);
+        for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
+        if (m_mc0.get()) result->m_mc0 = m_mc0->translate(tr);
+        result->m_internalized = m_internalized;
+        result->m_internalized_converted = m_internalized_converted;
         return result;
     }
 
@@ -272,7 +275,6 @@ public:
         m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER);
         m_params.set_bool("xor_solver", p1.xor_solver());
         m_solver.updt_params(m_params);
-        m_optimize_model = m_params.get_bool("optimize_model", false);
 
     }
     virtual void collect_statistics(statistics & st) const {
@@ -383,9 +385,9 @@ public:
         // extract original fixed variables
         u_map<expr*> asm2dep;
         extract_asm2dep(dep2asm, asm2dep);
-        for (unsigned i = 0; i < vars.size(); ++i) {
+        for (auto v : vars) {
             expr_ref cons(m);
-            if (extract_fixed_variable(dep2asm, asm2dep, vars[i], bool_var2conseq, lconseq, cons)) {
+            if (extract_fixed_variable(dep2asm, asm2dep, v, bool_var2conseq, lconseq, cons)) {
                 conseq.push_back(cons);
             }
         }
@@ -407,11 +409,10 @@ public:
         }
         vector<sat::literal_vector> ls_mutexes;
         m_solver.find_mutexes(ls, ls_mutexes);
-        for (unsigned i = 0; i < ls_mutexes.size(); ++i) {
-            sat::literal_vector const ls_mutex = ls_mutexes[i];
+        for (sat::literal_vector const& ls_mutex : ls_mutexes) {
             expr_ref_vector mutex(m);
-            for (unsigned j = 0; j < ls_mutex.size(); ++j) {
-                mutex.push_back(lit2var.find(ls_mutex[j].index()));
+            for (sat::literal l : ls_mutex) {
+                mutex.push_back(lit2var.find(l.index()));
             }
             mutexes.push_back(mutex);
         }