diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp
index 6bffd19ef..d901da0e9 100644
--- a/src/opt/opt_pareto.cpp
+++ b/src/opt/opt_pareto.cpp
@@ -110,88 +110,3 @@ namespace opt {
 
 }
 
-#if 0
-        opt_solver& s = get_solver();        
-        expr_ref val(m);
-        rational r;
-        lbool is_sat = l_true;
-        vector<bounds_t> bounds;
-        for (unsigned i = 0; i < m_objectives.size(); ++i) {
-            objective const& obj = m_objectives[i];
-            if (obj.m_type == O_MAXSMT) {
-                IF_VERBOSE(0, verbose_stream() << "Pareto optimization is not supported for MAXSMT\n";);
-                return l_undef;
-            }
-            solver::scoped_push _sp(s);
-            is_sat = m_optsmt.pareto(obj.m_index);
-            if (is_sat != l_true) {
-                return is_sat;
-            }
-            if (!m_optsmt.get_upper(obj.m_index).is_finite()) {
-                return l_undef;
-            }
-            bounds_t bound;            
-            for (unsigned j = 0; j < m_objectives.size(); ++j) {
-                objective const& obj_j = m_objectives[j];
-                inf_eps lo = m_optsmt.get_lower(obj_j.m_index);
-                inf_eps hi = m_optsmt.get_upper(obj_j.m_index);
-                bound.push_back(std::make_pair(lo, hi));
-            }            
-            bounds.push_back(bound);
-        }
-        for (unsigned i = 0; i < bounds.size(); ++i) {
-            for (unsigned j = 0; j < bounds.size(); ++j) {
-                objective const& obj = m_objectives[j];
-                bounds[i][j].second = bounds[j][j].second;                
-            }
-            IF_VERBOSE(0, display_bounds(verbose_stream() << "new bound\n", bounds[i]););
-        }
-
-        for (unsigned i = 0; i < bounds.size(); ++i) {
-            bounds_t b = bounds[i];
-            vector<inf_eps> mids;
-            solver::scoped_push _sp(s);
-            for (unsigned j = 0; j < b.size(); ++j) {
-                objective const& obj = m_objectives[j];
-                inf_eps mid = (b[j].second - b[j].first)/rational(2);
-                mids.push_back(mid);
-                expr_ref ge = s.mk_ge(obj.m_index, mid);            
-                s.assert_expr(ge);
-            }
-            is_sat = execute_box();
-            switch(is_sat) {
-            case l_undef: 
-                return is_sat;
-            case l_true: {
-                bool at_bound = true; 
-                for (unsigned j = 0; j < b.size(); ++j) {
-                    objective const& obj = m_objectives[j];
-                    if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
-                        mids[j] = inf_eps(r);
-                    }
-                    at_bound = at_bound && mids[j] == b[j].second;
-                    b[j].second = mids[j];
-                }
-                IF_VERBOSE(0, display_bounds(verbose_stream() << "new bound\n", b););
-                if (!at_bound) {
-                    bounds.push_back(b);
-                }
-                break;
-            }
-            case l_false: {
-                bounds_t b2(b);
-                for (unsigned j = 0; j < b.size(); ++j) {
-                    b2[j].second = mids[j];
-                    if (j > 0) {
-                        b2[j-1].second = b[j-1].second;
-                    }
-                    IF_VERBOSE(0, display_bounds(verbose_stream() << "refined bound\n", b2););
-                    bounds.push_back(b2);
-                }
-                break;
-            }
-            }
-        }
-        
-        return is_sat;
-#endif