diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 6bf4f6e1d..8a4f07b18 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -224,35 +224,26 @@ public:
         enable_sls(m_asms);
         set_mus(false);
         ptr_vector<expr> mcs;
-        while (m_lower < m_upper) {            
+        lbool is_sat = l_true;
+        while (m_lower < m_upper && is_sat == l_true) {            
             IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
+            vector<ptr_vector<expr> > cores;
+            ptr_vector<expr> mss;       
+            model_ref mdl;
+            expr_ref tmp(m);
+            mcs.reset();
+            s().get_model(mdl);
+            update_assignment(mdl.get());
+            mss.append(m_asms.size(), m_asms.c_ptr());
+            is_sat = m_mss(cores, mss, mcs);
 
-            lbool is_sat = s().check_sat(0, 0);
-            if (is_sat == l_true) {
-                vector<ptr_vector<expr> > cores;
-                ptr_vector<expr> mss;       
-                model_ref mdl;
-                expr_ref tmp(m);
-                mcs.reset();
-                s().get_model(mdl);
-                update_assignment(mdl.get());
-                for (unsigned i = 0; i < m_asms.size(); ++i) {
-                    VERIFY(mdl->eval(m_asms[i].get(), tmp));
-                    if (m.is_true(tmp)) {
-                        mss.push_back(m_asms[i].get());
-                    }
-                }
-                is_sat = m_mss(cores, mss, mcs);
-                std::cout << mcs.size() << " " << is_sat << "\n";
-            }
             switch (is_sat) {
             case l_undef:
                 return l_undef;
             case l_false:
                 m_lower = m_upper;
-                break;
-            case l_true: {
-                
+                return l_true;
+            case l_true: {                
                 is_sat = process_sat(mcs);
                 if (is_sat != l_true) {
                     return is_sat;
@@ -263,6 +254,12 @@ public:
                 break;
             }
             }
+            if (m_cancel) {
+                return l_undef;
+            }
+            if (m_lower < m_upper) {
+                is_sat = s().check_sat(0, 0);
+            }
         }
         m_lower = m_upper;
         return l_true;
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index e3c9e860c..44f898443 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -179,6 +179,9 @@ namespace opt {
     }
 
     void maxsmt::verify_assignment() {
+        // TBD: have to use a different solver 
+        // because we don't push local scope any longer.
+        return;
         solver::scoped_push _sp(m_s);
         commit_assignment();
         if (l_true != m_s.check_sat(0,0)) {
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 0110132f2..ee275e7f6 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -75,7 +75,6 @@ namespace opt {
         void set_model() { s().get_model(m_model); }
         virtual void updt_params(params_ref& p);
         virtual void init_soft(vector<rational> const& weights, expr_ref_vector const& soft);
-        void add_hard(expr* e){ s().assert_expr(e); }        
         solver& s() { return m_s; }
         void init();
         expr* mk_not(expr* e);
diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp
index 63a7a72bf..77dd39409 100644
--- a/src/opt/mss.cpp
+++ b/src/opt/mss.cpp
@@ -49,7 +49,7 @@ namespace opt {
         return true;
     }
 
-    void mss::initialize(vector<exprs>& cores, exprs& literals) {
+    void mss::initialize(exprs& literals) {
         expr* n;
         expr_set lits, core_lits;
         for (unsigned i = 0; i < literals.size(); ++i) {
@@ -67,8 +67,8 @@ namespace opt {
         // did not occur in previous cores and did not evaluate to true
         // in the current model.
         //
-        for (unsigned i = 0; i < cores.size(); ++i) {
-            exprs const& core = cores[i];
+        for (unsigned i = 0; i < m_cores.size(); ++i) {
+            exprs const& core = m_cores[i];
             for (unsigned j = 0; j < core.size(); ++j) {
                 expr* n = core[j];
                 if (!core_lits.contains(n)) {
@@ -97,7 +97,7 @@ namespace opt {
                 }
             }
         }
-        cores.push_back(rest_core);
+        m_cores.push_back(rest_core);
     }
 
     void mss::add_mss(expr* n) {
@@ -148,23 +148,20 @@ namespace opt {
         m_mss.reset();
         m_todo.reset();
         m_s.get_model(m_model);
+        m_cores.reset();
         SASSERT(m_model);
-        vector<exprs> cores(_cores);
+        m_cores.append(_cores);
+        initialize(literals);
         TRACE("opt", 
-              for (unsigned i = 0; i < cores.size(); ++i) {
-                  display_vec(tout << "core: ", cores[i].size(), cores[i].c_ptr());
-              }
               display_vec(tout << "lits: ", literals.size(), literals.c_ptr());
-              );
-        initialize(cores, literals);
-        TRACE("opt", display(tout););
+              display(tout););
         lbool is_sat = l_true;
-        for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
+        for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) {
             bool has_mcs = false;
-            bool is_last = i + 1 < cores.size();
+            bool is_last = i + 1 < m_cores.size();
             SASSERT(check_invariant());
-            update_core(cores[i]); // remove members of mss
-            is_sat = process_core(1, cores[i], has_mcs, is_last); 
+            update_core(m_cores[i]); // remove members of mss
+            is_sat = process_core(1, m_cores[i], has_mcs, is_last); 
         }    
         if (is_sat == l_true) {
             SASSERT(check_invariant());
@@ -180,6 +177,7 @@ namespace opt {
         }
         m_mcs.reset();
         m_mss_set.reset();
+        IF_VERBOSE(2, display_vec(verbose_stream() << "mcs: ", mcs.size(), mcs.c_ptr()););
         return is_sat;
     }
 
@@ -208,7 +206,7 @@ namespace opt {
         unsigned sz_save = m_mss.size();
         m_mss.append(sz, core.c_ptr());
         lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
-        IF_VERBOSE(2, display_vec(verbose_stream() << "mss: ", m_mss.size(), m_mss.c_ptr()););
+        IF_VERBOSE(3, display_vec(verbose_stream() << "mss: ", m_mss.size(), m_mss.c_ptr()););
         m_mss.resize(sz_save);
         switch (is_sat) {
         case l_true:
@@ -253,6 +251,9 @@ namespace opt {
     }
 
     void mss::display(std::ostream& out) const {
+        for (unsigned i = 0; i < m_cores.size(); ++i) {
+            display_vec(out << "core: ", m_cores[i].size(), m_cores[i].c_ptr());
+        }
         expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
         out << "mcs:\n";
         for (; it != end; ++it) {
@@ -261,7 +262,7 @@ namespace opt {
         out << "\n";
         out << "mss:\n";
         for (unsigned i = 0; i < m_mss.size(); ++i) {
-            out << mk_pp(m_mss[i], m) << "\n";
+           out << mk_pp(m_mss[i], m) << "\n";
         }
         out << "\n";
         if (m_model) {
diff --git a/src/opt/mss.h b/src/opt/mss.h
index cf69c14f9..057161eaa 100644
--- a/src/opt/mss.h
+++ b/src/opt/mss.h
@@ -29,6 +29,7 @@ namespace opt {
         exprs         m_mss;
         expr_set      m_mcs;
         expr_set      m_mss_set;
+        vector<exprs> m_cores;
         exprs         m_todo;
         model_ref     m_model;
     public:
@@ -42,7 +43,7 @@ namespace opt {
         void get_model(model_ref& mdl) { mdl = m_model; }
 
     private:
-        void  initialize(vector<exprs>& cores, exprs& literals);
+        void  initialize(exprs& literals);
         bool  check_result();
         void  add_mss(expr* n);
         void  update_mss();
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index d2de3ae80..327a636f7 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -436,6 +436,7 @@ namespace opt {
         }
         if (m_maxsat_engine != symbol("maxres") &&
             m_maxsat_engine != symbol("mus-mss-maxres") &&
+            m_maxsat_engine != symbol("mss-maxres") &&
             m_maxsat_engine != symbol("bcd2") &&
             m_maxsat_engine != symbol("sls")) {
             return;
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 84a1a4e52..c9cf44b2a 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -84,15 +84,12 @@ namespace opt {
         lbool operator()() {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
-            solver::scoped_push _s(s());
             lbool is_sat = l_true;
             bool was_sat = false;
             for (unsigned i = 0; i < m_soft.size(); ++i) {
                 wth().assert_weighted(m_soft[i].get(), m_weights[i]);
             }
-            solver::scoped_push __s(s());
             while (l_true == is_sat) {
-                IF_VERBOSE(1, verbose_stream() << "(opt.wmax [" << m_lower << ":" << m_upper << "])\n";);
                 is_sat = s().check_sat(0,0);
                 if (m_cancel) {
                     is_sat = l_undef;
@@ -106,6 +103,7 @@ namespace opt {
                     s().assert_expr(fml);
                     was_sat = true;
                 }
+                IF_VERBOSE(1, verbose_stream() << "(opt.wmax [" << m_lower << ":" << m_upper << "])\n";);
             }
             if (was_sat) {
                 wth().get_assignment(m_assignment);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index a0ba9c391..5b626f170 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -51,6 +51,7 @@ namespace sat {
         m_config.updt_params(p);
         m_conflicts_since_gc      = 0;
         m_next_simplify           = 0;
+        m_num_checkpoints         = 0;
     }
 
     solver::~solver() {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 5f45ab424..f7e6a009d 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -82,8 +82,8 @@ namespace sat {
         scc                     m_scc;
         asymm_branch            m_asymm_branch;
         probing                 m_probing;
-        mus                     m_mus;
-        wsls                    m_wsls;
+        mus                     m_mus;           // MUS for minimal core extraction
+        wsls                    m_wsls;          // SLS facility for MaxSAT use
         bool                    m_inconsistent;
         // A conflict is usually a single justification. That is, a justification
         // for false. If m_not_l is not null_literal, then m_conflict is a
@@ -123,9 +123,9 @@ namespace sat {
         stopwatch               m_stopwatch;
         params_ref              m_params;
         scoped_ptr<solver>      m_clone; // for debugging purposes
-        literal_vector          m_assumptions;
-        literal_set             m_assumption_set;
-        literal_vector          m_core;
+        literal_vector          m_assumptions;      // additional assumptions during check
+        literal_set             m_assumption_set;   // set of enabled assumptions
+        literal_vector          m_core;             // unsat core
 
         void del_clauses(clause * const * begin, clause * const * end);
 
@@ -230,6 +230,9 @@ namespace sat {
         clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
         void checkpoint() {
             if (m_cancel) throw solver_exception(Z3_CANCELED_MSG);
+            ++m_num_checkpoints;
+            if (m_num_checkpoints < 10) return;
+            m_num_checkpoints = 0;
             if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
         }
         typedef std::pair<literal, literal> bin_clause;
@@ -275,6 +278,7 @@ namespace sat {
         unsigned m_luby_idx;
         unsigned m_conflicts_since_gc;
         unsigned m_gc_threshold;
+        unsigned m_num_checkpoints;
         double   m_min_d_tk;
         unsigned m_next_simplify;
         bool decide();
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 0330141cb..7c7eca33b 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -69,6 +69,7 @@ class bit_blaster_tactic : public tactic {
             expr_ref   new_curr(m());
             proof_ref  new_pr(m());
             unsigned size = g->size();
+            bool change = false;
             for (unsigned idx = 0; idx < size; idx++) {
                 if (g->inconsistent())
                     break;
@@ -79,10 +80,13 @@ class bit_blaster_tactic : public tactic {
                     proof * pr = g->pr(idx);
                     new_pr     = m().mk_modus_ponens(pr, new_pr);
                 }
-                g->update(idx, new_curr, new_pr, g->dep(idx));
+                if (curr != new_curr) {
+                    change = true;
+                    g->update(idx, new_curr, new_pr, g->dep(idx));
+                }
             }
             
-            if (g->models_enabled())  
+            if (change && g->models_enabled())  
                 mc = mk_bit_blaster_model_converter(m(), m_rewriter.const2bits());
             else
                 mc = 0;