diff --git a/src/opt/bcd2.cpp b/src/opt/bcd2.cpp
index bf041a6bd..766e0d84a 100644
--- a/src/opt/bcd2.cpp
+++ b/src/opt/bcd2.cpp
@@ -187,7 +187,7 @@ namespace opt {
             expr_ref fml(m);
             expr* r = m_soft_aux[i].get();
             m_soft2index.insert(r, i);
-            fml = m.mk_or(r, m_soft[i].get()); 
+            fml = m.mk_or(r, m_soft[i]); 
             m_soft_constraints.push_back(fml);
             m_asm_set.insert(r);
             SASSERT(m_weights[i].is_int());     
@@ -233,7 +233,7 @@ namespace opt {
             new_assignment.reset();
             s().get_model(model);
             for (unsigned i = 0; i < m_soft.size(); ++i) {
-                VERIFY(model->eval(m_soft[i].get(), val));    
+                VERIFY(model->eval(m_soft[i], val));    
                 new_assignment.push_back(m.is_true(val));                            
                 if (!new_assignment[i]) {
                     new_upper += m_weights[i];
@@ -393,7 +393,7 @@ namespace opt {
                 out << "[" << c.m_lower << ":" << c.m_mid << ":" << c.m_upper << "]\n";
             }
             for (unsigned i = 0; i < m_soft.size(); ++i) {
-                out << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n";
+                out << mk_pp(m_soft[i], m) << " " << m_weights[i] << "\n";
             }
         }
     };
diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index b410a102e..6d2386b96 100644
--- a/src/opt/fu_malik.cpp
+++ b/src/opt/fu_malik.cpp
@@ -43,34 +43,24 @@ Notes:
 */
 namespace opt {
 
-    struct fu_malik::imp {
-        ast_manager&    m;        
-        solver&         m_s;
+    class fu_malik : public maxsmt_solver_base {
         filter_model_converter& m_fm;
-        expr_ref_vector m_soft;
-        expr_ref_vector m_orig_soft;
+        expr_ref_vector m_aux_soft;
         expr_ref_vector m_aux;
-        svector<bool>   m_assignment;
-        unsigned        m_upper;
-        unsigned        m_lower;
         model_ref       m_model;
 
-        imp(context& c, expr_ref_vector const& soft):
-            m(c.get_manager()),
-            m_s(c.get_solver()),
+    public:
+        fu_malik(context& c, weights_t& ws, expr_ref_vector const& soft):
+            maxsmt_solver_base(c, ws, soft),
             m_fm(c.fm()),
-            m_soft(soft),
-            m_orig_soft(soft),
-            m_aux(m),
-            m_upper(0),
-            m_lower(0) 
+            m_aux_soft(soft),
+            m_aux(m) 
         {
-            m_upper = m_soft.size() + 1;
-            m_assignment.resize(m_soft.size(), false);
+            m_upper = rational(m_aux_soft.size() + 1);
+            m_lower.reset();
+            m_assignment.resize(m_aux_soft.size(), false);
         }
 
-        solver& s() { return m_s; }
-
         /**
            \brief One step of the Fu&Malik algorithm.
            
@@ -96,9 +86,8 @@ namespace opt {
             }
         }
 
-
         void collect_statistics(statistics& st) const {
-            st.update("opt-fm-num-steps", m_soft.size() + 2 - m_upper);
+            st.update("opt-fm-num-steps", m_aux_soft.size() + 2 - m_upper.get_unsigned());
         }
 
         void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const {
@@ -115,9 +104,9 @@ namespace opt {
         }
 
         lbool step() {
-            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper << ")\n";);
+            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_aux_soft.size() + 2 - m_upper.get_unsigned() << ")\n";);
             expr_ref_vector assumptions(m), block_vars(m);
-            for (unsigned i = 0; i < m_soft.size(); ++i) {
+            for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
                 assumptions.push_back(m.mk_not(m_aux[i].get()));
             }
             lbool is_sat = s().check_sat(assumptions.size(), assumptions.c_ptr());
@@ -131,7 +120,7 @@ namespace opt {
             SASSERT(!core.empty());
 
             // Update soft-constraints and aux_vars
-            for (unsigned i = 0; i < m_soft.size(); ++i) {
+            for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
                 
                 bool found = false;
                 for (unsigned j = 0; !found && j < core.size(); ++j) {
@@ -145,14 +134,14 @@ namespace opt {
                 m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort());
                 m_fm.insert(block_var->get_decl());
                 m_fm.insert(to_app(m_aux[i].get())->get_decl());
-                m_soft[i] = m.mk_or(m_soft[i].get(), block_var);
+                m_aux_soft[i] = m.mk_or(m_aux_soft[i].get(), block_var);
                 block_vars.push_back(block_var);
-                tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
+                tmp = m.mk_or(m_aux_soft[i].get(), m_aux[i].get());
                 s().assert_expr(tmp);
             }
             SASSERT (!block_vars.empty());
             assert_at_most_one(block_vars);
-            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_soft.size() - block_vars.size() << ")\n";);
+            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_aux_soft.size() - block_vars.size() << ")\n";);
             return l_false;
         }
 
@@ -181,9 +170,9 @@ namespace opt {
         
 
         // TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
-        lbool operator()() {
+        virtual lbool operator()() {
             lbool is_sat = l_true;                
-            if (m_soft.empty()) {
+            if (m_aux_soft.empty()) {
                 return is_sat;
             }
             solver::scoped_push _sp(s());
@@ -191,14 +180,14 @@ namespace opt {
 
             TRACE("opt",
                   tout << "soft constraints:\n";
-                  for (unsigned i = 0; i < m_soft.size(); ++i) {
-                      tout << mk_pp(m_soft[i].get(), m) << "\n";
+                  for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
+                      tout << mk_pp(m_aux_soft[i].get(), m) << "\n";
                   });
 
-            for (unsigned i = 0; i < m_soft.size(); ++i) {
+            for (unsigned i = 0; i < m_aux_soft.size(); ++i) {
                 m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
                 m_fm.insert(to_app(m_aux.back())->get_decl());
-                tmp = m.mk_or(m_soft[i].get(), m_aux[i].get());
+                tmp = m.mk_or(m_aux_soft[i].get(), m_aux[i].get());
                 s().assert_expr(tmp);
             }
             
@@ -209,13 +198,13 @@ namespace opt {
             while (is_sat == l_false);
             
             if (is_sat == l_true) {
-                // Get a list satisfying m_soft
+                // Get a list satisfying m_aux_soft
                 s().get_model(m_model);
                 m_lower = m_upper;
                 m_assignment.reset();                    
-                for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
+                for (unsigned i = 0; i < m_soft.size(); ++i) {
                     expr_ref val(m);
-                    VERIFY(m_model->eval(m_orig_soft[i].get(), val));
+                    VERIFY(m_model->eval(m_soft[i], val));
                     TRACE("opt", tout << val << "\n";);
                     m_assignment.push_back(m.is_true(val));                        
                 }
@@ -227,43 +216,22 @@ namespace opt {
             return is_sat;            
         }
 
-        void get_model(model_ref& mdl) {
+        virtual void get_model(model_ref& mdl) {
             mdl = m_model.get();
         }
 
+        virtual rational get_lower() const {
+            return rational(m_aux_soft.size())-m_upper;
+        }
+
+        virtual rational get_upper() const {
+            return rational(m_aux_soft.size())-m_lower;
+        }
     };
 
-    fu_malik::fu_malik(context& c, expr_ref_vector& soft_constraints) {
-        m_imp = alloc(imp, c, soft_constraints);
-    }
-    fu_malik::~fu_malik() {
-        dealloc(m_imp);
-    }
-    
-    lbool fu_malik::operator()() {
-        return (*m_imp)();
-    }
-    rational fu_malik::get_lower() const {
-        return rational(m_imp->m_soft.size()-m_imp->m_upper);
-    }
-    rational fu_malik::get_upper() const {
-        return rational(m_imp->m_soft.size()-m_imp->m_lower);
-    }
-    bool fu_malik::get_assignment(unsigned idx) const {
-        return m_imp->m_assignment[idx];
-    }
-    void fu_malik::set_cancel(bool f) {
-        // no-op
-    }
-    void fu_malik::collect_statistics(statistics& st) const {
-        m_imp->collect_statistics(st);
-    }
-    void fu_malik::get_model(model_ref& m) {
-        m_imp->get_model(m);
+    maxsmt_solver_base* mk_fu_malik(context& c, weights_t & ws, expr_ref_vector const& soft) {
+        return alloc(fu_malik, c, ws, soft);
     }
 
-    void fu_malik::updt_params(params_ref& p) {
-        // no-op
-    }
 };
 
diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h
index 8eb363cb6..5eea9fc49 100644
--- a/src/opt/fu_malik.h
+++ b/src/opt/fu_malik.h
@@ -29,21 +29,8 @@ Notes:
 
 namespace opt {
 
-    class fu_malik : public maxsmt_solver {
-        struct imp;
-        imp* m_imp;
-    public:
-        fu_malik(context& c, expr_ref_vector& soft_constraints);
-        virtual ~fu_malik();
-        virtual lbool operator()();
-        virtual rational get_lower() const;
-        virtual rational get_upper() const;
-        virtual bool get_assignment(unsigned idx) const;
-        virtual void set_cancel(bool f);
-        virtual void collect_statistics(statistics& st) const;
-        virtual void get_model(model_ref& m);
-        virtual void updt_params(params_ref& p);
-    };
+    maxsmt_solver_base* mk_fu_malik(context& c, weights_t & ws, expr_ref_vector const& soft);
+
     
 };
 
diff --git a/src/opt/maxhs.cpp b/src/opt/maxhs.cpp
index a7425b22e..6d4a7b8bf 100644
--- a/src/opt/maxhs.cpp
+++ b/src/opt/maxhs.cpp
@@ -162,7 +162,7 @@ namespace opt {
             m_aux2index.reset();
             m_core_activity.reset();
             for (unsigned i = 0; i < sz; ++i) {
-                bool tt = is_true(m_model, m_soft[i].get());
+                bool tt = is_true(m_model, m_soft[i]);
                 m_seed.push_back(tt);
                 m_aux. push_back(mk_fresh(m.mk_bool_sort()));
                 m_aux_active.push_back(false);
@@ -380,7 +380,7 @@ namespace opt {
                 if (m_seed[i]) {
                     // already an assumption
                 }
-                else if (is_true(mdl, m_soft[i].get())) {
+                else if (is_true(mdl, m_soft[i])) {
                     m_seed[i] = true;                    
                     m_asms.push_back(m_aux[i].get());
                 }
@@ -420,7 +420,7 @@ namespace opt {
             }
             DEBUG_CODE(                
                 for (unsigned i = 0; i < num_soft(); ++i) {
-                    SASSERT(is_true(mdl, m_soft[i].get()) == m_seed[i]);
+                    SASSERT(is_true(mdl, m_soft[i]) == m_seed[i]);
                 });
             
             return true;
@@ -545,7 +545,7 @@ namespace opt {
         void ensure_active(unsigned i) {
             if (!is_active(i)) {
                 expr_ref fml(m);
-                fml = m.mk_implies(m_aux[i].get(), m_soft[i].get());
+                fml = m.mk_implies(m_aux[i].get(), m_soft[i]);
                 s().assert_expr(fml);
                 m_aux_active[i] = true;
             }
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 79c0ccd72..86c0efb8f 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -84,6 +84,7 @@ private:
     expr_ref_vector  m_trail;
     strategy_t       m_st;
     rational         m_max_upper;
+    bool             m_found_feasible_optimum;
     bool             m_hill_climb;             // prefer large weight soft clauses for cores
     bool             m_add_upper_bound_block;  // restrict upper bound with constraint
     unsigned         m_max_num_cores;          // max number of cores per round.
@@ -105,6 +106,7 @@ public:
         m_mss(c.get_solver(), m),
         m_trail(m),
         m_st(st),
+        m_found_feasible_optimum(false),
         m_hill_climb(true),
         m_add_upper_bound_block(false),
         m_max_num_cores(UINT_MAX),
@@ -122,6 +124,8 @@ public:
             (m.is_not(l, l) && is_uninterp_const(l));
     }
 
+    
+
     void add_soft(expr* e, rational const& w) {
         TRACE("opt", tout << mk_pp(e, m) << "\n";);
         expr_ref asum(m), fml(m);
@@ -372,13 +376,14 @@ public:
                 SASSERT(is_true(m_asms[i].get()));
             });
         for (unsigned i = 0; i < m_soft.size(); ++i) {
-            m_assignment[i] = is_true(m_soft[i].get());
+            m_assignment[i] = is_true(m_soft[i]);
         }
         m_upper = m_lower;
+        m_found_feasible_optimum = true;
     }
 
 
-    lbool operator()() {
+    virtual lbool operator()() {
         switch(m_st) {
         case s_mus:
             return mus_solver();
@@ -781,7 +786,7 @@ public:
         rational upper(0);
         expr_ref tmp(m);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
-            expr* n = m_soft[i].get();
+            expr* n = m_soft[i];
             VERIFY(mdl->eval(n, tmp));
             if (!m.is_true(tmp)) {
                 upper += m_weights[i];
@@ -796,7 +801,7 @@ public:
         m_model = mdl;
 
         for (unsigned i = 0; i < m_soft.size(); ++i) {
-            m_assignment[i] = is_true(m_soft[i].get());
+            m_assignment[i] = is_true(m_soft[i]);
         }
         m_upper = upper;
         // verify_assignment();
@@ -811,7 +816,7 @@ public:
         expr_ref_vector nsoft(m);
         expr_ref fml(m);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
-            nsoft.push_back(mk_not(m, m_soft[i].get()));
+            nsoft.push_back(mk_not(m, m_soft[i]));
         }            
         fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
         s().assert_expr(fml);        
@@ -864,12 +869,25 @@ public:
         m_lower.reset();
         m_trail.reset();
         for (unsigned i = 0; i < m_soft.size(); ++i) {
-            add_soft(m_soft[i].get(), m_weights[i]);
+            add_soft(m_soft[i], m_weights[i]);
         }
         m_max_upper = m_upper;
+        m_found_feasible_optimum = false;
         add_upper_bound_block();
     }
 
+    virtual void commit_assignment() {
+        if (m_found_feasible_optimum) {
+            TRACE("opt", tout << "Committing feasible solution\n";);
+            for (unsigned i = 0; i < m_asms.size(); ++i) {
+                s().assert_expr(m_asms[i].get());
+            }
+        }
+        else {
+            maxsmt_solver_base::commit_assignment();
+        }
+    }
+
     void verify_assignment() {
         IF_VERBOSE(0, verbose_stream() << "verify assignment\n";);        
         ref<solver> sat_solver = mk_inc_sat_solver(m, m_params);
@@ -878,7 +896,7 @@ public:
         }
         expr_ref n(m);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
-            n = m_soft[i].get();
+            n = m_soft[i];
             if (!m_assignment[i]) {
                 n = mk_not(m, n);
             }
diff --git a/src/opt/maxsls.cpp b/src/opt/maxsls.cpp
index 1c6e745a4..fc9c71607 100644
--- a/src/opt/maxsls.cpp
+++ b/src/opt/maxsls.cpp
@@ -41,7 +41,7 @@ namespace opt {
                 m_upper.reset();
                 for (unsigned i = 0; i < m_soft.size(); ++i) {
                     expr_ref tmp(m);
-                    m_model->eval(m_soft[i].get(), tmp, true);
+                    m_model->eval(m_soft[i], tmp, true);
                     m_assignment[i] = m.is_true(tmp);
                     if (!m_assignment[i]) {
                         m_upper += m_weights[i];
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index d8bc1073f..46b782dfd 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -30,6 +30,7 @@ Notes:
 #include "opt_context.h"
 #include "theory_wmaxsat.h"
 #include "ast_util.h"
+#include "pb_decl_plugin.h"
 
 
 namespace opt {
@@ -38,12 +39,13 @@ namespace opt {
         context& c, vector<rational> const& ws, expr_ref_vector const& soft):
         m(c.get_manager()), 
         m_c(c),
-        m_cancel(false), m_soft(m),
+        m_cancel(false), 
+        m_soft(soft),
+        m_weights(ws),
         m_assertions(m) {
         c.get_base_model(m_model);
         SASSERT(m_model);
         updt_params(c.params());
-        init_soft(ws, soft);
     }
     
     void maxsmt_solver_base::updt_params(params_ref& p) {
@@ -54,11 +56,17 @@ namespace opt {
         return m_c.get_solver(); 
     }
 
-    void maxsmt_solver_base::init_soft(vector<rational> const& weights, expr_ref_vector const& soft) {
-        m_weights.reset();
-        m_soft.reset();
-        m_weights.append(weights);
-        m_soft.append(soft);
+    void maxsmt_solver_base::commit_assignment() {
+        expr_ref tmp(m);
+        rational k(0);
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            if (get_assignment(i)) {
+                k += m_weights[i];
+            }
+        }       
+        pb_util pb(m);
+        tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k);
+        s().assert_expr(tmp);
     }
 
     void maxsmt_solver_base::init() {
@@ -67,7 +75,7 @@ namespace opt {
         m_assignment.reset();
         for (unsigned i = 0; i < m_weights.size(); ++i) {
             expr_ref val(m);
-            VERIFY(m_model->eval(m_soft[i].get(), val));                
+            VERIFY(m_model->eval(m_soft[i], val));                
             m_assignment.push_back(m.is_true(val));
             if (!m_assignment.back()) {
                 m_upper += m_weights[i];
@@ -178,7 +186,7 @@ namespace opt {
             m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
         }        
         else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("fu_malik")) {
-            m_msolver = alloc(fu_malik, m_c, m_soft_constraints);
+            m_msolver = mk_fu_malik(m_c, m_weights, m_soft_constraints);
         }
         else {
             if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
@@ -217,12 +225,6 @@ namespace opt {
         // TBD: have to use a different solver 
         // because we don't push local scope any longer.
         return;
-        solver::scoped_push _sp(s());
-        commit_assignment();
-        if (l_true != s().check_sat(0,0)) {
-            IF_VERBOSE(0, verbose_stream() << "could not verify assignment\n";);
-            UNREACHABLE();
-        }
     }
 
     bool maxsmt::get_assignment(unsigned idx) const {
@@ -265,14 +267,8 @@ namespace opt {
     }
 
     void maxsmt::commit_assignment() {
-        for (unsigned i = 0; i < m_soft_constraints.size(); ++i) {
-            expr_ref tmp(m);
-            tmp = m_soft_constraints[i].get();
-            if (!get_assignment(i)) {
-                tmp = mk_not(m, tmp);
-            }
-            TRACE("opt", tout << "committing: " << tmp << "\n";);
-            s().assert_expr(tmp);            
+        if (m_msolver) {
+            m_msolver->commit_assignment();
         }
     }
 
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 6341d0756..6a19a223b 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -61,9 +61,9 @@ namespace opt {
         ast_manager&     m;
         context&         m_c;
         volatile bool    m_cancel;
-        expr_ref_vector  m_soft;
-        expr_ref_vector  m_assertions;
+        const expr_ref_vector  m_soft;
         vector<rational> m_weights;
+        expr_ref_vector  m_assertions;
         rational         m_lower;
         rational         m_upper;
         model_ref        m_model;
@@ -80,9 +80,9 @@ namespace opt {
         virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); }
         virtual void collect_statistics(statistics& st) const { }
         virtual void get_model(model_ref& mdl) { mdl = m_model.get(); }
+        virtual void commit_assignment();
         void set_model() { s().get_model(m_model); }
         virtual void updt_params(params_ref& p);
-        virtual void init_soft(weights_t& weights, expr_ref_vector const& soft);
         solver& s();
         void init();
         void set_mus(bool f);
@@ -114,7 +114,7 @@ namespace opt {
     class maxsmt {
         ast_manager&              m;
         context&                  m_c;
-        scoped_ptr<maxsmt_solver> m_msolver;
+        scoped_ptr<maxsmt_solver_base> m_msolver;
         volatile bool    m_cancel;
         expr_ref_vector  m_soft_constraints;
         expr_ref_vector  m_answer;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 5004ceb32..7fcbe918b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -1204,10 +1204,7 @@ namespace opt {
                 maxsmt& ms = *m_maxsmts.find(obj.m_id);
                 for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
                     VERIFY(m_model->eval(obj.m_terms[i], val));
-                    CTRACE("opt",ms.get_assignment(i) != (m.mk_true() == val), 
-                           tout << mk_pp(obj.m_terms[i], m) << " evaluates to " << val << "\n";
-                           model_smt2_pp(tout, m, *m_model, 0););
-                    SASSERT(ms.get_assignment(i) == (m.mk_true() == val));
+                    // TBD: check that optimal was not changed.
                 }
                 break;
             }
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 78675387c..48d46a6c9 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -43,7 +43,7 @@ namespace opt {
             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]);
+                wth().assert_weighted(m_soft[i], m_weights[i]);
             }
             while (l_true == is_sat) {
                 is_sat = s().check_sat(0,0);