diff --git a/src/opt/bcd2.cpp b/src/opt/bcd2.cpp
index 779654e7e..bf041a6bd 100644
--- a/src/opt/bcd2.cpp
+++ b/src/opt/bcd2.cpp
@@ -124,7 +124,7 @@ namespace opt {
             }
             process_sat();
             while (m_lower < m_upper) {
-                IF_VERBOSE(1, verbose_stream() << "(opt.bcd2 [" << m_lower << ":" << m_upper << "])\n";);
+                trace_bounds("bcd2");
                 assert_soft();
                 solver::scoped_push _scope2(s());
                 TRACE("opt", display(tout););
diff --git a/src/opt/core_maxsat.cpp b/src/opt/core_maxsat.cpp
deleted file mode 100644
index 0663f9abc..000000000
--- a/src/opt/core_maxsat.cpp
+++ /dev/null
@@ -1,168 +0,0 @@
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    core_maxsat.h
-
-Abstract:
-
-    Core and SAT guided MaxSAT with cardinality constraints.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2013-11-9
-
-Notes:
-
---*/
-#include "core_maxsat.h"
-#include "pb_decl_plugin.h"
-#include "ast_pp.h"
-#include "opt_context.h"
-
-namespace opt {
-        
-    core_maxsat::core_maxsat(context& c, expr_ref_vector& soft_constraints):
-        m(c.get_manager()), s(c.get_solver()), 
-        m_lower(0), m_upper(soft_constraints.size()), m_soft(soft_constraints) {
-        m_answer.resize(m_soft.size(), false);
-    }
-    
-    core_maxsat::~core_maxsat() {}
-    
-    lbool core_maxsat::operator()() {
-        expr_ref_vector aux(m);         // auxiliary variables to track soft constraints
-        expr_set core_vars;             // variables used so far in some core
-        expr_set block_vars;            // variables that should be blocked.
-        solver::scoped_push _sp(s);
-        for (unsigned i = 0; i < m_soft.size(); ++i) {
-            expr* a = m.mk_fresh_const("p", m.mk_bool_sort());
-            aux.push_back(m.mk_not(a));
-            s.assert_expr(m.mk_or(a, m_soft[i].get()));
-            block_vars.insert(aux.back());
-        }            
-        while (m_lower < m_upper) {
-            ptr_vector<expr> vars;
-            set2vector(block_vars, vars);
-            lbool is_sat = s.check_sat(vars.size(), vars.c_ptr());
-            
-            switch(is_sat) {
-            case l_undef: 
-                return l_undef;
-            case l_true: {
-                model_ref mdl;
-                svector<bool> ans;
-                unsigned new_lower = 0;
-                s.get_model(mdl);
-                for (unsigned i = 0; i < aux.size(); ++i) {
-                    expr_ref val(m);
-                    VERIFY(mdl->eval(m_soft[i].get(), val));
-                    ans.push_back(m.is_true(val));
-                    if (ans.back()) ++new_lower;
-                }
-                TRACE("opt", tout << "sat\n";
-                      for (unsigned i = 0; i < ans.size(); ++i) {
-                          tout << mk_pp(m_soft[i].get(), m) << " |-> " << ans[i] << "\n";
-                      });
-                IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat with lower bound: " << new_lower << "\n";);
-                if (new_lower > m_lower) {
-                    m_answer.reset();
-                    m_answer.append(ans);
-                    m_model = mdl.get();
-                    m_lower = new_lower;
-                }
-                if (m_lower == m_upper) {
-                    return l_true;
-                }
-                SASSERT(m_soft.size() >= new_lower+1);
-                unsigned k = m_soft.size()-new_lower-1;
-                expr_ref fml = mk_at_most(core_vars, k);
-                TRACE("opt", tout << "add: " << fml << "\n";);
-                s.assert_expr(fml);
-                break;                    
-            }
-            case l_false: {
-                ptr_vector<expr> core;
-                s.get_unsat_core(core);
-                TRACE("opt", tout << "core";
-                      for (unsigned i = 0; i < core.size(); ++i) {
-                          tout << mk_pp(core[i], m) << " ";
-                      }
-                      tout << "\n";);
-                for (unsigned i = 0; i < core.size(); ++i) {
-                    core_vars.insert(get_not(core[i]));
-                    block_vars.remove(core[i]);
-                }
-                IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
-                if (core.empty()) {
-                    m_upper = m_lower;
-                    return l_true;
-                }
-                else {
-                    // at least one core variable is True
-                    expr_ref fml = mk_at_most(core_vars, 0);
-                    fml = m.mk_not(fml);
-                    TRACE("opt", tout << "add: " << fml << "\n";);
-                    s.assert_expr(fml);
-                }
-                --m_upper;                
-            }
-            }            
-        }
-        return l_true;
-    }
-    
-    void core_maxsat::set2vector(expr_set const& set, ptr_vector<expr>& es) const {
-        es.reset();
-        expr_set::iterator it = set.begin(), end = set.end();
-        for (; it != end; ++it) {
-            es.push_back(*it);
-        }
-    }
-
-    expr_ref core_maxsat::mk_at_most(expr_set const& set, unsigned k) {
-        pb_util pb(m);
-        ptr_vector<expr> es;
-        set2vector(set, es);
-        return expr_ref(pb.mk_at_most_k(es.size(), es.c_ptr(), k), m);
-    }
-
-    expr* core_maxsat::get_not(expr* e) const {
-        expr* result = 0;
-        VERIFY(m.is_not(e, result));
-        return result;
-    }
-    
-    rational core_maxsat::get_lower() const {
-        return rational(m_soft.size()-m_upper);
-    }
-    rational core_maxsat::get_upper() const {
-        return rational(m_soft.size()-m_lower);
-    }
-    bool core_maxsat::get_assignment(unsigned idx) const {
-        return m_answer[idx];
-    }
-    void core_maxsat::set_cancel(bool f) {
-        
-    }
-    void core_maxsat::collect_statistics(statistics& st) const {
-        // nothing specific
-    }
-    void core_maxsat::updt_params(params_ref& p) {
-        // no-op
-    }
-    void core_maxsat::get_model(model_ref& mdl) {
-        mdl = m_model.get();
-        if (!mdl) {
-            SASSERT(m_upper == 0);
-            lbool is_sat = s.check_sat(0, 0);
-            if (is_sat == l_true) {
-                s.get_model(m_model);
-            }
-            mdl = m_model;
-        }
-    }
-
-    
-};
diff --git a/src/opt/core_maxsat.h b/src/opt/core_maxsat.h
deleted file mode 100644
index bbb173a3f..000000000
--- a/src/opt/core_maxsat.h
+++ /dev/null
@@ -1,55 +0,0 @@
-/*++
-Copyright (c) 2013 Microsoft Corporation
-
-Module Name:
-
-    core_maxsat.h
-
-Abstract:
-    Core and SAT guided MaxSAT with cardinality constraints.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2013-11-9
-
-Notes:
-
---*/
-#ifndef _OPT_CORE_MAXSAT_H_
-#define _OPT_CORE_MAXSAT_H_
-
-#include "solver.h"
-#include "maxsmt.h"
-
-namespace opt {
-
-    class core_maxsat : public maxsmt_solver {
-        typedef obj_hashtable<expr> expr_set;
-
-        ast_manager&    m;
-        solver&         s;
-        expr_ref_vector m_soft;
-        svector<bool>   m_answer;
-        unsigned        m_upper;
-        unsigned        m_lower;
-        model_ref       m_model;
-    public:
-        core_maxsat(context& c, expr_ref_vector& soft_constraints);
-        virtual ~core_maxsat();
-        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& mdl);
-        virtual void updt_params(params_ref& p);
-    private:
-        void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
-        expr_ref mk_at_most(expr_set const& set, unsigned k);
-        expr* get_not(expr* e) const;
-    };
-    
-};
-
-#endif
diff --git a/src/opt/maxhs.cpp b/src/opt/maxhs.cpp
index 9f8aa2d11..a7425b22e 100644
--- a/src/opt/maxhs.cpp
+++ b/src/opt/maxhs.cpp
@@ -111,8 +111,7 @@ namespace opt {
             seed2assumptions();
             while (m_lower < m_upper) {
                 ++m_stats.m_num_iterations;
-                IF_VERBOSE(1, verbose_stream() << 
-                           "(opt.maxhs [" << m_lower << ":" << m_upper << "])\n";);
+                trace_bounds("maxhs");
                 TRACE("opt", tout << "(maxhs [" << m_lower << ":" << m_upper << "])\n";);
                 if (m_cancel) {
                     return l_undef;
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 48dbb410b..60cc11555 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -193,7 +193,7 @@ public:
         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";);
+            trace_bounds("maxres");
             if (m_cancel) {
                 return l_undef;
             }
@@ -512,7 +512,7 @@ public:
         fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
         s().assert_expr(fml);
         m_lower += w;
-        IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
+        trace_bounds("maxres");
     }
 
     bool get_mus_model(model_ref& mdl) {
@@ -789,8 +789,7 @@ public:
         }
         m_upper = upper;
         // verify_assignment();
-        IF_VERBOSE(1, verbose_stream() << 
-                   "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
+        trace_bounds("maxres");
 
         add_upper_bound_block();
     }
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index d128e57f2..e737f9efe 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -20,11 +20,9 @@ Notes:
 #include <typeinfo>
 #include "maxsmt.h"
 #include "fu_malik.h"
-#include "core_maxsat.h"
 #include "maxres.h"
 #include "maxhs.h"
 #include "bcd2.h"
-#include "pbmax.h"
 #include "wmax.h"
 #include "maxsls.h"
 #include "ast_pp.h"
@@ -140,6 +138,13 @@ namespace opt {
     }
     smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
     
+    void maxsmt_solver_base::trace_bounds(char const * solver) {
+        IF_VERBOSE(1, 
+                   rational l = m_adjust_value(m_lower);
+                   rational u = m_adjust_value(m_upper);
+                   if (l > u) std::swap(l, u);
+                   verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);        
+    }
 
 
 
@@ -167,9 +172,6 @@ namespace opt {
         else if (maxsat_engine == symbol("mss-maxres")) {            
             m_msolver = mk_mss_maxres(m_c, m_weights, m_soft_constraints);
         }
-        else if (maxsat_engine == symbol("pbmax")) {
-            m_msolver = mk_pbmax(m_c, m_weights, m_soft_constraints);
-        }
         else if (maxsat_engine == symbol("bcd2")) {
             m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints);
         }
@@ -180,9 +182,6 @@ namespace opt {
             // NB: this is experimental one-round version of SLS
             m_msolver = mk_sls(m_c, m_weights, m_soft_constraints);
         }        
-        else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("core_maxsat")) {
-            m_msolver = alloc(core_maxsat, m_c, 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);
         }
@@ -196,6 +195,7 @@ namespace opt {
 
         if (m_msolver) {
             m_msolver->updt_params(m_params);
+            m_msolver->set_adjust_value(m_adjust_value);
             is_sat = (*m_msolver)();
             if (is_sat != l_false) {
                 m_msolver->get_model(m_model);
@@ -245,7 +245,7 @@ namespace opt {
             rational q = m_msolver->get_lower();
             if (q > r) r = q;
         }
-        return r;
+        return m_adjust_value(r);
     }
 
     rational maxsmt::get_upper() const {
@@ -254,17 +254,16 @@ namespace opt {
             rational q = m_msolver->get_upper();
             if (q < r) r = q;
         }
-        return r;
+        return m_adjust_value(r);
     }
 
-    void maxsmt::update_lower(rational const& r, bool override) {
-        if (m_lower > r || override)  m_lower = r;
+    void maxsmt::update_lower(rational const& r) {
+        if (m_lower > r) m_lower = r;
     }
 
-    void maxsmt::update_upper(rational const& r, bool override) {
-        if (m_upper < r || override)  m_upper = r;
-    }
-    
+    void maxsmt::update_upper(rational const& r) {
+        if (m_upper < r) m_upper = r;
+    }    
 
     void maxsmt::get_model(model_ref& mdl) {
         mdl = m_model.get();
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 2b868408a..4c0d8d825 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -27,6 +27,7 @@ Notes:
 #include"smt_context.h"
 #include"smt_theory.h"
 #include"theory_wmaxsat.h"
+#include"opt_solver.h"
 
 namespace opt {
 
@@ -35,6 +36,8 @@ namespace opt {
     class context;
 
     class maxsmt_solver {
+    protected:
+        adjust_value m_adjust_value;
     public:        
         virtual ~maxsmt_solver() {}
         virtual lbool operator()() = 0;
@@ -45,6 +48,7 @@ namespace opt {
         virtual void collect_statistics(statistics& st) const = 0;
         virtual void get_model(model_ref& mdl) = 0;
         virtual void updt_params(params_ref& p) = 0;
+        void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
 
     };
 
@@ -100,6 +104,7 @@ namespace opt {
     protected:
         void enable_sls(expr_ref_vector const& soft, weights_t& ws);
         void set_enable_sls(bool f);
+        void trace_bounds(char const* solver);
 
     };
 
@@ -119,6 +124,7 @@ namespace opt {
         vector<rational> m_weights;
         rational         m_lower;
         rational         m_upper;
+        adjust_value     m_adjust_value;
         model_ref        m_model;
         params_ref       m_params;
     public:
@@ -127,15 +133,16 @@ namespace opt {
         void set_cancel(bool f);
         void updt_params(params_ref& p);
         void add(expr* f, rational const& w); 
+        void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
         unsigned size() const { return m_soft_constraints.size(); }
         expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
         rational weight(unsigned idx) const { return m_weights[idx]; }
         void commit_assignment();
         rational get_value() const;
         rational get_lower() const;
-        rational get_upper() const;
-        void update_lower(rational const& r, bool override);
-        void update_upper(rational const& r, bool override);
+        rational get_upper() const;        
+        void update_lower(rational const& r);
+        void update_upper(rational const& r);
         void get_model(model_ref& mdl);
         bool get_assignment(unsigned index) const;
         void display_answer(std::ostream& out) const;        
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index ca4b40740..b71826e9b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -218,7 +218,7 @@ namespace opt {
         IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";);
         s.get_model(m_model);
         m_optsmt.setup(*m_opt_solver.get());
-        update_lower(true);
+        update_lower();
         switch (m_objectives.size()) {
         case 0:
             return is_sat;
@@ -293,7 +293,7 @@ namespace opt {
                 return r;
             }
             if (r == l_true && i + 1 < m_objectives.size()) {
-                update_lower(true);
+                update_lower();
             }
         }
         DEBUG_CODE(if (r == l_true) validate_lex(););
@@ -398,8 +398,8 @@ namespace opt {
 
     void context::yield() {
         m_pareto->get_model(m_model);
-        update_bound(true, true);
-        update_bound(true, false);
+        update_bound(true);
+        update_bound(false);
     }
 
     lbool context::execute_pareto() {
@@ -763,8 +763,9 @@ namespace opt {
                 SASSERT(obj.m_id == id);
                 obj.m_terms.reset();
                 obj.m_terms.append(terms);
-                obj.m_adjust_bound.set_offset(offset);
-                obj.m_adjust_bound.set_negate(neg);
+                obj.m_adjust_value.set_offset(offset);
+                obj.m_adjust_value.set_negate(neg);
+                m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value);
                 TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";);
             }
             else if (is_maximize(fml, tr, orig_term, index)) {
@@ -772,6 +773,7 @@ namespace opt {
             }
             else if (is_minimize(fml, tr, orig_term, index)) {
                 m_objectives[index].m_term = tr;
+                m_objectives[index].m_adjust_value.set_negate(true);
             }
             else {
                 m_hard_constraints.push_back(fml);
@@ -826,15 +828,16 @@ namespace opt {
         }
     }
 
-    void context::update_bound(bool override, bool is_lower) {
+    void context::update_bound(bool is_lower) {
         expr_ref val(m);
+        bool override = true;
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];
             rational r;
             switch(obj.m_type) {
             case O_MINIMIZE:
                 if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
-                    inf_eps val = obj.m_adjust_bound.neg_add(r);
+                    inf_eps val = inf_eps(obj.m_adjust_value(r));
                     if (is_lower) {
                         m_optsmt.update_lower(obj.m_index, val, override);
                     }
@@ -845,7 +848,7 @@ namespace opt {
                 break;
             case O_MAXIMIZE:
                 if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
-                    inf_eps val = obj.m_adjust_bound.neg_add(r);
+                    inf_eps val = inf_eps(obj.m_adjust_value(r));
                     if (is_lower) {
                         m_optsmt.update_lower(obj.m_index, val, override);
                     }
@@ -868,10 +871,10 @@ namespace opt {
                 }
                 if (ok) {
                     if (is_lower) {
-                        m_maxsmts.find(obj.m_id)->update_upper(r, override);
+                        m_maxsmts.find(obj.m_id)->update_upper(r);
                     }
                     else {
-                        m_maxsmts.find(obj.m_id)->update_lower(r, override);
+                        m_maxsmts.find(obj.m_id)->update_lower(r);
                     }
                 }
                 break;
@@ -918,14 +921,12 @@ namespace opt {
         }
         objective const& obj = m_objectives[idx];
         switch(obj.m_type) {
-        case O_MAXSMT: {
-            rational r = m_maxsmts.find(obj.m_id)->get_lower();
-            return obj.m_adjust_bound.neg_add(r);
-        }
+        case O_MAXSMT: 
+            return inf_eps(m_maxsmts.find(obj.m_id)->get_lower());
         case O_MINIMIZE:
-            return -m_optsmt.get_upper(obj.m_index);
+            return obj.m_adjust_value(m_optsmt.get_upper(obj.m_index));
         case O_MAXIMIZE: 
-            return m_optsmt.get_lower(obj.m_index);
+            return obj.m_adjust_value(m_optsmt.get_lower(obj.m_index));
         default:
             UNREACHABLE();
             return inf_eps();
@@ -939,12 +940,11 @@ namespace opt {
         objective const& obj = m_objectives[idx];
         switch(obj.m_type) {
         case O_MAXSMT: 
-            return obj.m_adjust_bound.neg_add(m_maxsmts.find(obj.m_id)->get_upper());
-            // TBD: adjust bound
+            return inf_eps(m_maxsmts.find(obj.m_id)->get_upper());
         case O_MINIMIZE:
-            return -m_optsmt.get_lower(obj.m_index);
+            return obj.m_adjust_value(m_optsmt.get_lower(obj.m_index));
         case O_MAXIMIZE: 
-            return m_optsmt.get_upper(obj.m_index);
+            return obj.m_adjust_value(m_optsmt.get_upper(obj.m_index));
         default:
             UNREACHABLE();
             return inf_eps();
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 051729aff..eb8dd6fc6 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -51,7 +51,7 @@ namespace opt {
             app_ref     m_term;          // for maximize, minimize term
             expr_ref_vector   m_terms;   // for maxsmt
             vector<rational>  m_weights; // for maxsmt
-            bound_adjustment  m_adjust_bound;
+            adjust_value  m_adjust_value;
             symbol      m_id;            // for maxsmt
             unsigned    m_index;         // for maximize/minimize index
 
@@ -63,7 +63,7 @@ namespace opt {
                 m_index(idx)
             {
                 if (!is_max) {
-                    m_adjust_bound.set_negate(true);
+                    m_adjust_value.set_negate(true);
                 }
             }
 
@@ -212,8 +212,8 @@ namespace opt {
         void from_fmls(expr_ref_vector const& fmls);
         void simplify_fmls(expr_ref_vector& fmls);
 
-        void update_lower(bool override) { update_bound(override, true); }
-        void update_bound(bool override, bool is_lower);
+        void update_lower() { update_bound(true); }
+        void update_bound(bool is_lower);
 
         inf_eps get_lower_as_num(unsigned idx);
         inf_eps get_upper_as_num(unsigned idx);
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 0e59a9eb9..29b450e08 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -36,30 +36,31 @@ namespace opt {
 
     typedef inf_eps_rational<inf_rational> inf_eps;
 
-    // Adjust bound bound |-> (m_negate?-1:1)*(m_offset + bound)
-    class bound_adjustment {
+    // Adjust bound bound |-> m_offset + (m_negate?-1:1)*bound
+    class adjust_value {
         rational m_offset;
         bool     m_negate;
     public:
-        bound_adjustment(rational const& offset, bool neg):
+        adjust_value(rational const& offset, bool neg):
             m_offset(offset),
             m_negate(neg)
         {}
-        bound_adjustment(): m_offset(0), m_negate(false) {}
+        adjust_value(): m_offset(0), m_negate(false) {}
         void set_offset(rational const& o) { m_offset = o; }
         void set_negate(bool neg) { m_negate = neg; }
         rational const& get_offset() const { return m_offset; }
         bool get_negate() { return m_negate; }
-        inf_eps add_neg(rational const& r) const {
-            rational result = r + m_offset;
+        inf_eps operator()(inf_eps const& r) const {
+            inf_eps result = r;
             if (m_negate) result.neg();
-            return inf_eps(result);
+            result += m_offset;
+            return result;
         }
-        inf_eps neg_add(rational const& r) const {
+        rational operator()(rational const& r) const {
             rational result = r;
             if (m_negate) result.neg();
             result += m_offset;
-            return inf_eps(result);
+            return result;
         }
     };
 
diff --git a/src/opt/pbmax.cpp b/src/opt/pbmax.cpp
deleted file mode 100644
index a30fe3acb..000000000
--- a/src/opt/pbmax.cpp
+++ /dev/null
@@ -1,95 +0,0 @@
-/*++
-Copyright (c) 2014 Microsoft Corporation
-
-Module Name:
-
-    pbmax.cpp
-
-Abstract:
-
-    pb based MaxSAT.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2014-4-17
-
-Notes:
-
---*/
-#include "pbmax.h"
-#include "pb_decl_plugin.h"
-#include "uint_set.h"
-#include "ast_pp.h"
-#include "model_smt2_pp.h"
-
-
-namespace opt {
-
-    // ----------------------------------
-    // incrementally add pseudo-boolean 
-    // lower bounds.
-
-    class pbmax : public maxsmt_solver_base {
-    public:
-        pbmax(context& c, weights_t& ws, expr_ref_vector const& soft): 
-            maxsmt_solver_base(c, ws, soft) {
-        }
-        
-        virtual ~pbmax() {}
-
-        lbool operator()() {
-
-            TRACE("opt", s().display(tout); tout << "\n";
-                  for (unsigned i = 0; i < m_soft.size(); ++i) {
-                      tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n";
-                  }
-                  );
-            pb_util u(m);
-            expr_ref fml(m), val(m);
-            app_ref b(m);
-            expr_ref_vector nsoft(m);
-            init();            
-            for (unsigned i = 0; i < m_soft.size(); ++i) {
-                nsoft.push_back(mk_not(m_soft[i].get()));
-            }
-            lbool is_sat = l_true;
-            while (l_true == is_sat) {
-                TRACE("opt", s().display(tout<<"looping\n"); 
-                      model_smt2_pp(tout << "\n", m, *(m_model.get()), 0););
-                m_upper.reset();
-                for (unsigned i = 0; i < m_soft.size(); ++i) {
-                    VERIFY(m_model->eval(nsoft[i].get(), val));
-                    m_assignment[i] = !m.is_true(val);
-                    if (!m_assignment[i]) {
-                        m_upper += m_weights[i];
-                    }
-                }                     
-                IF_VERBOSE(1, verbose_stream() << "(opt.pb [" << m_lower << ":" << m_upper << "])\n";);
-                TRACE("opt", tout << "new upper: " << m_upper << "\n";);
-                
-                fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
-                solver::scoped_push _scope2(s());
-                s().assert_expr(fml);
-                is_sat = s().check_sat(0,0);
-                if (m_cancel) {
-                    is_sat = l_undef;
-                }
-                if (is_sat == l_true) {
-                    s().get_model(m_model);
-                }
-            }            
-            if (is_sat == l_false) {
-                is_sat = l_true;
-                m_lower = m_upper;
-            }
-            TRACE("opt", tout << "lower: " << m_lower << "\n";);
-            return is_sat;
-        }
-    };
-
-    maxsmt_solver_base* mk_pbmax(
-        context & c, weights_t& ws, expr_ref_vector const& soft) {
-        return alloc(pbmax, c, ws, soft);
-    }
-
-}
diff --git a/src/opt/pbmax.h b/src/opt/pbmax.h
deleted file mode 100644
index 78d43b045..000000000
--- a/src/opt/pbmax.h
+++ /dev/null
@@ -1,29 +0,0 @@
-/*++
-Copyright (c) 2014 Microsoft Corporation
-
-Module Name:
-
-    pbmax.h
-
-Abstract:
-
-    MaxSAT based on pb theory.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2014-4-17
-
-Notes:
-
---*/
-
-#ifndef _PBMAX_H_
-#define _PBMAX_H_
-
-#include "maxsmt.h"
-
-namespace opt {
-    maxsmt_solver_base* mk_pbmax(context& c, weights_t& ws, expr_ref_vector const& soft);
-
-}
-#endif
diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp
index 3499c51ff..78675387c 100644
--- a/src/opt/wmax.cpp
+++ b/src/opt/wmax.cpp
@@ -59,7 +59,7 @@ namespace opt {
                     s().assert_expr(fml);
                     was_sat = true;
                 }
-                IF_VERBOSE(1, verbose_stream() << "(opt.wmax [" << m_lower << ":" << m_upper << "])\n";);
+                trace_bounds("wmax");
             }
             if (was_sat) {
                 wth().get_assignment(m_assignment);