diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index d2db3a603..50bfee20e 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1056,6 +1056,11 @@ namespace smt {
     inf_eps_rational<inf_rational> theory_arith<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
         TRACE("bound_bug", display_var(tout, v); display(tout););
         has_shared = false;
+        if (!m_nl_monomials.empty()) {
+            has_shared = true;
+            blocker = mk_gt(v);
+            return inf_eps_rational<inf_rational>(get_value(v));            
+        }
         max_min_t r = max_min(v, true, true, has_shared); 
         if (r == UNBOUNDED) {
             has_shared = false;
@@ -1300,6 +1305,7 @@ namespace smt {
 
     */
 
+
     
     template<typename Ext>
     bool theory_arith<Ext>::pick_var_to_leave(
@@ -1331,7 +1337,7 @@ namespace smt {
             if (update_gains(inc, s, coeff_ij, min_gain, max_gain) ||
                 (x_i == null_theory_var && !unbounded_gain(max_gain))) {
                 x_i = s;
-                a_ij = coeff_ij;
+                a_ij = coeff_ij;                
             }
             has_shared |= ctx.is_shared(get_enode(s));
         }