diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 4d64cbab9..b666e14e4 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -88,6 +88,8 @@ private:
     bool             m_all_cores;
     bool             m_add_upper_bound_block;
 
+    typedef ptr_vector<expr> exprs;
+
 public:
     maxres(context& c,
            weights_t& ws, expr_ref_vector const& soft, 
@@ -176,8 +178,8 @@ public:
         init();
         init_local();
         sls();
-        ptr_vector<expr> mcs;
-        vector<ptr_vector<expr> > cores;
+        exprs mcs;
+        vector<exprs> cores;
         while (m_lower < m_upper) {            
             TRACE("opt", 
                   display_vec(tout, m_asms.size(), m_asms.c_ptr());
@@ -219,19 +221,18 @@ public:
         init_local();
         sls();
         set_mus(false);
-        ptr_vector<expr> mcs;
+        exprs mcs;
         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;       
+            vector<exprs> cores;
+            exprs 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);
+            is_sat = get_mss(cores, mss, mcs);
 
             switch (is_sat) {
             case l_undef:
@@ -244,9 +245,7 @@ public:
                 if (is_sat != l_true) {
                     return is_sat;
                 }
-                model_ref mdl;
-                m_mss.get_model(mdl);
-                update_assignment(mdl.get());
+                update_mss_model();
                 break;
             }
             }
@@ -285,11 +284,12 @@ public:
     */
     lbool mus_mss2_solver() {
         m_all_cores = true;
-        m_add_upper_bound_block = true;
+        //m_add_upper_bound_block = true;
         init();
         init_local();
         sls();
-        vector<ptr_vector<expr> > cores;
+        vector<exprs> cores;
+        m_mus.set_soft(m_soft.size(), m_soft.c_ptr(), m_weights.c_ptr());
         lbool is_sat = l_true;
         while (m_lower < m_upper && is_sat == l_true) {            
             TRACE("opt", 
@@ -307,7 +307,7 @@ public:
                 found_optimum();
                 return l_true;
             case l_false:
-                is_sat = process_unsat(cores);
+                is_sat = get_cores(cores);
                 break;
             default:
                 break;
@@ -315,27 +315,42 @@ public:
             if (is_sat == l_undef) {
                 return l_undef;
             }
+            SASSERT((is_sat == l_false) == cores.empty());
+            SASSERT((is_sat == l_true) == !cores.empty());
             if (cores.empty()) {
-                SASSERT(is_sat == l_false);
                 break;
             }
-            SASSERT(is_sat == l_true);
 
-            // TBD: there is some best model, 
-            // retrieve it from the get_cores calls.
-            // extend it to a maximal assignment
-            // extracting the mss and mcs.
-
-            set_mus(false);
-            ptr_vector<expr> mss, mcs;
-            is_sat = m_mss(cores, mss, mcs);
-            set_mus(true);
+            //
+            // There is a best model, 
+            // retrieve it from the previous 
+            // core calls.
+            //
+            update_mus_model();
+            // 
+            // Extend the current model to a (maximal)
+            // assignment extracting the ss and cs.
+            // ss - satisfying subset
+            // cs - correction set (complement of it).
+            //
+            exprs ss, cs;
+            is_sat = get_mss(cores, ss, cs);
+            if (is_sat != l_true) return is_sat;
+            update_mss_model();
+            //
+            // block the hard constraints corresponding to the cores.
+            // block the soft constraints corresponding to the cs.
+            // The original cs is not disjoint from the cores, 
+            // after the cores are blocked, the soft constraints 
+            // are changed.
+            // 
+            is_sat = process_unsat(cores);
+            if (is_sat != l_true) return is_sat;
+            get_current_correction_set(cs);
+            is_sat = process_sat(cs);                        
             if (is_sat != l_true) return is_sat;
-            model_ref mdl;
-            m_mss.get_model(mdl); // last model is best way to reduce search space.
-            update_assignment(mdl.get());
-            is_sat = process_sat(mcs);            
         }
+        
         m_lower = m_upper;
         return l_true;
     }
@@ -370,12 +385,12 @@ public:
         return l_undef;
     }
 
-    lbool get_cores(vector<ptr_vector<expr> >& cores) {
+    lbool get_cores(vector<exprs>& cores) {
         // assume m_s is unsat.
         lbool is_sat = l_false;
         expr_ref_vector asms(m_asms);
         cores.reset();
-        ptr_vector<expr> core;
+        exprs core;
         while (is_sat == l_false) {
             core.reset();
             s().get_unsat_core(core);
@@ -420,6 +435,18 @@ public:
         return is_sat;
     }
 
+    void get_current_correction_set(exprs& cs) {
+        TRACE("opt", display_vec(tout << "old correction set: ", cs.size(), cs.c_ptr()););
+        cs.reset();
+        expr_ref tmp(m);
+        for (unsigned i = 0; i < m_asms.size(); ++i) {
+            VERIFY(m_model->eval(m_asms[i].get(), tmp));
+            if (!m.is_true(tmp)) {
+                cs.push_back(m_asms[i].get());
+            }
+        }
+        TRACE("opt", display_vec(tout << "new correction set: ", cs.size(), cs.c_ptr()););
+    }
 
     struct compare_asm {
         maxres& mr;
@@ -431,7 +458,7 @@ public:
 
     void sort_assumptions(expr_ref_vector& _asms) {
         compare_asm comp(*this);
-        ptr_vector<expr> asms(_asms.size(), _asms.c_ptr());
+        exprs asms(_asms.size(), _asms.c_ptr());
         expr_ref_vector trail(_asms);
         std::sort(asms.begin(), asms.end(), comp);
         _asms.reset();
@@ -451,7 +478,7 @@ public:
         return index;
     }
 
-    lbool process_sat(ptr_vector<expr> const& corr_set) {
+    lbool process_sat(exprs const& corr_set) {
         expr_ref fml(m), tmp(m);
         TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
         remove_core(corr_set);
@@ -461,11 +488,7 @@ public:
     }
 
     lbool process_unsat() {
-        vector<ptr_vector<expr> > cores;
-        return process_unsat(cores);
-    }
-
-    lbool process_unsat(vector<ptr_vector<expr> >& cores) {
+        vector<exprs> cores;
         lbool is_sat = get_cores(cores);
         if (is_sat != l_true) {
             return is_sat;
@@ -473,13 +496,20 @@ public:
         if (cores.empty()) {
             return l_false;
         }
+        else {
+            return process_unsat(cores);
+        }
+    }
+
+    lbool process_unsat(vector<exprs>& cores) {
+        lbool is_sat = l_true;
         for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
             is_sat = process_unsat(cores[i]);
         }
         return is_sat;
     }
     
-    lbool process_unsat(ptr_vector<expr> const& core) {
+    lbool process_unsat(exprs const& core) {
         expr_ref fml(m);
         remove_core(core);
         SASSERT(!core.empty());
@@ -493,7 +523,33 @@ public:
         return l_true;
     }
 
-    lbool minimize_core(ptr_vector<expr>& core) {
+    void update_mus_model() {
+        if (!m_c.sat_enabled()) {
+            model_ref mdl;
+            rational w = m_mus.get_best_model(mdl);
+            if (mdl.get() && w < m_upper) {
+                update_assignment(mdl.get());
+            }
+        }
+    }
+
+    void update_mss_model() {
+        model_ref mdl;
+        m_mss.get_model(mdl); // last model is best way to reduce search space.
+        update_assignment(mdl.get());
+    }
+
+    lbool get_mss(vector<exprs> const& cores, exprs& literals, exprs& mcs) {
+        literals.reset();
+        mcs.reset();
+        literals.append(m_asms.size(), m_asms.c_ptr());
+        set_mus(false);
+        lbool is_sat = m_mss(m_model.get(), cores, literals, mcs);
+        set_mus(true);
+        return is_sat;
+    }
+
+    lbool minimize_core(exprs& core) {
         if (m_c.sat_enabled() || core.empty()) {
             return l_true;
         }
@@ -527,7 +583,7 @@ public:
         enable_sls(m_asms, ws);
     }
 
-    rational split_core(ptr_vector<expr> const& core) {
+    rational split_core(exprs const& core) {
         if (core.empty()) return rational(0);
         // find the minimal weight:
         rational w = get_weight(core[0]);
@@ -562,7 +618,7 @@ public:
         }
     }
 
-    void max_resolve(ptr_vector<expr> const& core, rational const& w) {
+    void max_resolve(exprs const& core, rational const& w) {
         SASSERT(!core.empty());
         expr_ref fml(m), asum(m);
         app_ref cls(m), d(m), dd(m);
@@ -604,7 +660,7 @@ public:
     }
 
     // cs is a correction set (a complement of a (maximal) satisfying assignment).
-    void cs_max_resolve(ptr_vector<expr> const& cs, rational const& w) {
+    void cs_max_resolve(exprs const& cs, rational const& w) {
         if (cs.empty()) return;
         TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr()););
         expr_ref fml(m), asum(m);
@@ -645,10 +701,10 @@ public:
         s().assert_expr(fml);
     }
 
-    lbool try_improve_bound(vector<ptr_vector<expr> >& cores, ptr_vector<expr>& mcs) {
+    lbool try_improve_bound(vector<exprs>& cores, exprs& mcs) {
         cores.reset();
         mcs.reset();
-        ptr_vector<expr> core;
+        exprs core;
         expr_ref_vector asms(m_asms);
         while (true) {
             rational upper = m_max_upper;
@@ -662,16 +718,15 @@ public:
                 model_ref mdl;
                 s().get_model(mdl); // last model is best way to reduce search space.
                 update_assignment(mdl.get());
-                ptr_vector<expr> mss;
+                exprs mss;
                 mss.append(asms.size(), asms.c_ptr());
                 set_mus(false);
-                is_sat = m_mss(cores, mss, mcs);
+                is_sat = m_mss(m_model.get(), cores, mss, mcs);
                 set_mus(true);
                 if (is_sat != l_true) {
                     return is_sat;
                 }
-                m_mss.get_model(mdl); // last model is best way to reduce search space.
-                update_assignment(mdl.get());
+                update_mss_model();
                 if (!cores.empty() && mcs.size() > cores.back().size()) {
                     mcs.reset();
                 }
@@ -753,7 +808,7 @@ public:
         }
     }
 
-    void remove_soft(ptr_vector<expr> const& core, expr_ref_vector& asms) {
+    void remove_soft(exprs const& core, expr_ref_vector& asms) {
         for (unsigned i = 0; i < asms.size(); ++i) {
             if (core.contains(asms[i].get())) {
                 asms[i] = asms.back();
@@ -763,7 +818,7 @@ public:
         }
     }
 
-    void remove_core(ptr_vector<expr> const& core) {
+    void remove_core(exprs const& core) {
         remove_soft(core, m_asms);
     }
 
@@ -811,7 +866,7 @@ opt::maxsmt_solver_base* opt::mk_maxres(
 
 opt::maxsmt_solver_base* opt::mk_mus_mss_maxres(
     context& c, weights_t& ws, expr_ref_vector const& soft) {
-    return alloc(maxres, c, ws, soft, maxres::s_mus_mss);
+    return alloc(maxres, c, ws, soft, maxres::s_mus_mss2);
 }
 
 opt::maxsmt_solver_base* opt::mk_mss_maxres(
diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp
index 77dd39409..3597aa6b9 100644
--- a/src/opt/mss.cpp
+++ b/src/opt/mss.cpp
@@ -144,10 +144,10 @@ namespace opt {
         m_todo.resize(j);
     }       
     
-    lbool mss::operator()(vector<exprs> const& _cores, exprs& literals, exprs& mcs) {
+    lbool mss::operator()(model* initial_model, vector<exprs> const& _cores, exprs& literals, exprs& mcs) {
         m_mss.reset();
         m_todo.reset();
-        m_s.get_model(m_model);
+        m_model = initial_model;
         m_cores.reset();
         SASSERT(m_model);
         m_cores.append(_cores);
diff --git a/src/opt/mss.h b/src/opt/mss.h
index 057161eaa..02d218e4d 100644
--- a/src/opt/mss.h
+++ b/src/opt/mss.h
@@ -36,7 +36,7 @@ namespace opt {
         mss(solver& s, ast_manager& m);
         ~mss();
         
-        lbool operator()(vector<exprs> const& cores, exprs& literals, exprs& mcs);
+        lbool operator()(model* initial_model, vector<exprs> const& cores, exprs& literals, exprs& mcs);
                 
         void set_cancel(bool f) { m_cancel = f; }