diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 1625b6440..9603286d1 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -28,6 +28,7 @@ namespace opt {
         lbool is_sat;
         m_answer.reset();
         m_msolver = 0;
+        m_s = &s;
         if (m_soft_constraints.empty()) {
             m_msolver = 0;
             is_sat = s.check_sat(0, 0);
@@ -80,8 +81,9 @@ namespace opt {
     }
 
     void maxsmt::commit_assignment() {
+        SASSERT(m_s);
         for (unsigned i = 0; i < m_answer.size(); ++i) {
-            s->assert_expr(m_answer[i].get());
+            m_s->assert_expr(m_answer[i].get());
         }
     }
 
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index 3d67ee7eb..e3105847d 100644
--- a/src/opt/maxsmt.h
+++ b/src/opt/maxsmt.h
@@ -41,14 +41,14 @@ namespace opt {
 
     class maxsmt {
         ast_manager&     m;
-        solver*          s;
+        solver*          m_s;
         volatile bool    m_cancel;
         expr_ref_vector  m_soft_constraints;
         expr_ref_vector  m_answer;
         vector<rational> m_weights;
         scoped_ptr<maxsmt_solver> m_msolver;
     public:
-        maxsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
+        maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
 
         lbool operator()(solver& s);
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2c64f8277..ebbccdb5d 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -51,8 +51,13 @@ namespace opt {
     }
 
     lbool context::optimize() {
-        // TBD: add configuration parameter to select between box and pareto
-        return optimize_box();
+        // TBD: does not work...
+        if (m_params.get_bool("pareto", false)) {
+            return optimize_pareto();
+        }
+        else {
+            return optimize_box();
+        }
     }
 
     lbool context::optimize_box() {
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index ae6e43aea..3c2381040 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -3,6 +3,7 @@ def_module_params('opt',
                   export=True,
                   params=(('timeout', UINT, UINT_MAX, 'set timeout'),
                           ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
+                          ('pareto', BOOL, False, 'return a Pareto front (as opposed to a bounding box)'),
                           ))
 
 
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index e291b76a5..15d8f6617 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -204,13 +204,7 @@ namespace opt {
     lbool optsmt::operator()(opt_solver& solver) {
         s = &solver;
         s->reset_objectives();
-        m_lower.reset();
-        m_upper.reset();
         m_vars.reset();
-        for (unsigned i = 0; i < m_objs.size(); ++i) {
-            m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
-            m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
-        }
 
         // First check_sat call to initialize theories
         lbool is_sat = s->check_sat(0, 0);
@@ -297,6 +291,8 @@ namespace opt {
         SASSERT(is_app(t2));
         m_objs.push_back(to_app(t2));
         m_is_max.push_back(is_max);
+        m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
+        m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
     }
 
     void optsmt::updt_params(params_ref& p) {
diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h
index 189da0e0e..0fbfeb7b2 100644
--- a/src/opt/optsmt.h
+++ b/src/opt/optsmt.h
@@ -51,7 +51,7 @@ namespace opt {
         void display_assignment(std::ostream& out) const;
         void display_range_assignment(std::ostream& out) const;
 
-        unsigned get_num_objectives() const { return m_vars.size(); }
+        unsigned get_num_objectives() const { return m_objs.size(); }
         void commit_assignment(unsigned index);
         inf_eps get_value(unsigned index) const;
         inf_eps get_lower(unsigned index) const;