diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 64978b39e..e61289f02 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -843,7 +843,6 @@ namespace opt {
     void context::update_bound(bool is_lower) {
         expr_ref val(m);
         if (!m_model.get()) return;
-        bool override = true;
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];
             rational r;
@@ -852,10 +851,10 @@ namespace opt {
                 if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
                     inf_eps val = inf_eps(obj.m_adjust_value(r));
                     if (is_lower) {
-                        m_optsmt.update_lower(obj.m_index, val, override);
+                        m_optsmt.update_lower(obj.m_index, val);
                     }
                     else {
-                        m_optsmt.update_upper(obj.m_index, val, override);
+                        m_optsmt.update_upper(obj.m_index, val);
                     }
                 }
                 break;
@@ -863,10 +862,10 @@ namespace opt {
                 if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) {
                     inf_eps val = inf_eps(obj.m_adjust_value(r));
                     if (is_lower) {
-                        m_optsmt.update_lower(obj.m_index, val, override);
+                        m_optsmt.update_lower(obj.m_index, val);
                     }
                     else {
-                        m_optsmt.update_upper(obj.m_index, val, override);
+                        m_optsmt.update_upper(obj.m_index, val);
                     }
                 }
                 break;
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 90f410cf5..615acc61d 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -48,7 +48,7 @@ namespace opt {
 
     void optsmt::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src, expr_ref_vector& fmls) {
         for (unsigned i = 0; i < src.size(); ++i) {
-            if (src[i] > dst[i]) {
+            if (src[i] >= dst[i]) {
                 dst[i] = src[i];
                 m_lower_fmls[i] = fmls[i].get();
                 if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already.
@@ -60,7 +60,6 @@ namespace opt {
                 fmls[i] = m_lower_fmls[i].get();
             }
         }
-        std::cout << "\n";
     }
 
     /*
@@ -170,16 +169,13 @@ namespace opt {
         return basic_opt();
     }
 
-    void optsmt::update_lower(unsigned idx, inf_eps const& v, bool override) {
-        if (m_lower[idx] < v || override) {
-            m_lower[idx] = v;            
-        }
+    void optsmt::update_lower(unsigned idx, inf_eps const& v) {
+        m_lower_fmls[idx] = m_s->mk_ge(idx, v);
+        m_lower[idx] = v;                    
     }
 
-    void optsmt::update_upper(unsigned idx, inf_eps const& v, bool override) {
-        if (m_upper[idx] > v || override) {
-            m_upper[idx] = v;            
-        }
+    void optsmt::update_upper(unsigned idx, inf_eps const& v) {
+        m_upper[idx] = v;                    
     }
 
     void optsmt::update_lower() {
diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h
index 4f982f695..7b8238992 100644
--- a/src/opt/optsmt.h
+++ b/src/opt/optsmt.h
@@ -60,8 +60,8 @@ namespace opt {
         inf_eps get_upper(unsigned index) const;
         void    get_model(model_ref& mdl);
 
-        void update_lower(unsigned idx, inf_eps const& r, bool override);
-        void update_upper(unsigned idx, inf_eps const& r, bool override);
+        void update_lower(unsigned idx, inf_eps const& r);
+        void update_upper(unsigned idx, inf_eps const& r);
 
         void reset();