diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index ebbccdb5d..7e62605ac 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -51,8 +51,7 @@ namespace opt {
     }
 
     lbool context::optimize() {
-        // TBD: does not work...
-        if (m_params.get_bool("pareto", false)) {
+        if (m_params.get_bool("pareto", false)) {            
             return optimize_pareto();
         }
         else {
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 15d8f6617..1380080ba 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -209,11 +209,11 @@ namespace opt {
         // First check_sat call to initialize theories
         lbool is_sat = s->check_sat(0, 0);
         if (is_sat == l_true && !m_objs.empty()) {
-            solver::scoped_push _push(*s);
-            
             for (unsigned i = 0; i < m_objs.size(); ++i) {
                 m_vars.push_back(s->add_objective(m_objs[i].get()));
-            }
+            }            
+
+            solver::scoped_push _push(*s);
 
             if (m_engine == symbol("basic")) {
                 is_sat = basic_opt();
@@ -249,8 +249,31 @@ namespace opt {
 
     // force lower_bound(i) <= objective_value(i)    
     void optsmt::commit_assignment(unsigned i) {
-        smt::theory_var v = m_vars[i];
-        s->assert_expr(s->block_upper_bound(i, get_lower(i)));
+        inf_eps mid(0);
+
+        // TBD: case analysis should be revisited
+        rational hi = get_upper(i).get_infinity();
+        rational lo = get_lower(i).get_infinity(); 
+        if (hi.is_pos() && !lo.is_neg()) {
+            mid = get_lower(i);
+        }
+        else if (hi.is_pos() && lo.is_neg()) {
+            mid = inf_eps(0);
+        }
+        else if (hi.is_pos() && lo.is_pos()) {
+            mid = inf_eps(0); // TBD: get a value from a model?
+        }
+        else if (hi.is_neg() && lo.is_neg()) {
+            mid = inf_eps(0); // TBD: get a value from a model?
+        }
+        else {
+            mid = hi;
+        }
+        m_lower[i] = mid;
+        m_upper[i] = mid;
+        TRACE("opt", tout << "set lower bound of "; display_objective(tout, i) << " to: " << mid << "\n";
+              tout << get_lower(i) << ":" << get_upper(i) << "\n";);
+        s->assert_expr(s->block_upper_bound(i, mid));
     }
 
     std::ostream& optsmt::display_objective(std::ostream& out, unsigned i) const {
diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h
index 268bb8109..9f40404ba 100644
--- a/src/util/inf_eps_rational.h
+++ b/src/util/inf_eps_rational.h
@@ -303,12 +303,12 @@ class inf_eps_rational {
     }
 
     friend inline rational floor(const inf_eps_rational & r) {
-        SASSERT(r.m_infty.is_zero());
+        // SASSERT(r.m_infty.is_zero());
         return floor(r.m_r);
     }
 
     friend inline rational ceil(const inf_eps_rational & r) {
-        SASSERT(r.m_infty.is_zero());
+        // SASSERT(r.m_infty.is_zero());
         return ceil(r.m_r);
     }