diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 6159c436e..1bd55b9bb 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -333,12 +333,13 @@ namespace lp {
         if (improve_lower_bound)
             term.negate();
         impq bound;
-        if (!maximize_term_on_tableau(term, bound))
+        if (!maximize_term_on_corrected_r_solver(term, bound))
             return false;
         
         return false;
         // TODO
         if (improve_lower_bound) {
+            bound.neg();
             if (column_has_lower_bound(j) && bound.x == column_lower_bound(j).x)
                 return false;
             SASSERT(!column_has_lower_bound(j) || column_lower_bound(j).x < bound.x);
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 1b34272df..61afa8859 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1548,7 +1548,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
     if (no_effect())
         m_monomial_bounds();
 
-    if (l_vec.empty() && !done() && improve_bounds())
+    if (no_effect() && improve_bounds())
         return l_false;
     
     {