diff --git a/src/opt/mss.cpp b/src/opt/mss.cpp
index cc0fa8d7d..47f4b6e02 100644
--- a/src/opt/mss.cpp
+++ b/src/opt/mss.cpp
@@ -155,10 +155,10 @@ namespace opt {
         lbool is_sat = l_true;
         for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) {
             bool has_mcs = false;
-            bool is_last = i + 1 < m_cores.size();
+            bool not_last = i + 1 < m_cores.size();
             SASSERT(check_invariant());
             update_core(m_cores[i]); // remove members of mss
-            is_sat = process_core(1, m_cores[i], has_mcs, is_last); 
+            is_sat = process_core(1, m_cores[i], has_mcs, not_last);
         }    
         if (is_sat == l_true) {
             SASSERT(check_invariant());
@@ -183,7 +183,7 @@ namespace opt {
     // at least one literal in core is false in current model.
     // pick literals in core that are not yet in mss.
     //    
-    lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) {
+    lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool not_last) {
         SASSERT(sz > 0);
         if (core.empty()) {
             return l_true;
@@ -191,7 +191,7 @@ namespace opt {
         if (m.canceled()) {
             return l_undef;
         }
-        if (sz == 1 && core.size() == 1 && is_last && !has_mcs) {
+        if (sz == 1 && core.size() == 1 && not_last && !has_mcs) {
             // there has to be at least one false 
             // literal in the core.
             TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";);
@@ -214,7 +214,7 @@ namespace opt {
                     SASSERT(m_mss_set.contains(core[i]));
                 });
             update_core(core);
-            return process_core(2*sz, core, has_mcs, is_last);
+            return process_core(2*sz, core, has_mcs, not_last);
         case l_false:
             if (sz == 1) {
                 has_mcs = true;
@@ -232,7 +232,7 @@ namespace opt {
                 }
                 update_core(core);
             }
-            return process_core(1, core, has_mcs, is_last);
+            return process_core(1, core, has_mcs, not_last);
         case l_undef:
             return l_undef;
         }
diff --git a/src/opt/mss_solver.cpp b/src/opt/mss_solver.cpp
index 501b43ee4..d27b6300c 100755
--- a/src/opt/mss_solver.cpp
+++ b/src/opt/mss_solver.cpp
@@ -98,15 +98,61 @@ private:
         vector<exprs> dummy;
         push_exprs(mss, m_asms);
         push_exprs(mss, asms);
-        is_sat = m_mss(mdl.get(), dummy, mss, mcs);
-        SASSERT(is_sat == l_true);
-        mdl.reset();
-        m_mss.get_model(mdl);
-        update_assignment(mdl.get());
-        IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
+        is_sat = cld(mdl.get(), mss, mcs);
+        if (is_sat == l_true) {
+            IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
+        }
+        /*is_sat = m_mss(mdl.get(), dummy, mss, mcs);
+        SASSERT(is_sat != l_false);
+        if (is_sat == l_true) {
+            mdl.reset();
+            m_mss.get_model(mdl);
+            update_assignment(mdl.get());
+            IF_VERBOSE(2, verbose_stream() << "(opt.mss-solver :mss " << mss.size() - asms.size() << " :mcs " << mcs.size() << ")\n";);
+        }*/
         return is_sat;
     }
 
+    lbool cld(model_ref initial_model, exprs& mss, exprs& mcs) {
+        exprs sat, undef;
+        undef.append(mss);
+        update_sat(initial_model, sat, undef);
+        lbool is_sat = l_true;
+        while (is_sat == l_true) {
+            expr_ref asum = relax_and_assert(m.mk_or(undef.size(), undef.c_ptr()));
+            sat.push_back(asum);
+            is_sat = check_sat(sat);
+            sat.pop_back();
+            if (is_sat == l_true) {
+                model_ref mdl;
+                s().get_model(mdl);
+                update_sat(mdl, sat, undef);
+                update_assignment(mdl.get());
+            }
+        }
+        if (is_sat == l_false) {
+            mss.reset();
+            mcs.reset();
+            mss.append(sat);
+            mcs.append(undef);
+            is_sat = l_true;
+        }
+        return is_sat;
+    }
+
+    void update_sat(model_ref mdl, exprs& sat, exprs& undef) {
+        for (unsigned i = 0; i < undef.size();) {
+            if (is_true(mdl.get(), undef[i])) {
+                sat.push_back(undef[i]);
+                undef[i] = undef.back();
+                undef.pop_back();
+            }
+            else {
+                ++i;
+            }
+        }
+    }
+
     void push_exprs(exprs& dst, expr_ref_vector const& src) {
         for (unsigned i = 0; i < src.size(); ++i) {
             dst.push_back(src[i]);
@@ -122,6 +168,10 @@ private:
         return s().check_sat(asms);
     }
 
+    lbool check_sat(exprs const& asms) {
+        return s().check_sat(asms.size(), asms.c_ptr());
+    }
+
     void update_assignment(model* mdl) {
         rational upper(0);
         for (unsigned i = 0; i < m_soft.size(); ++i) {