diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 8d0011ec1..cf2ec7ff4 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -993,7 +993,7 @@ namespace smt {
         // Optimization
         //
         // -----------------------------------
-        virtual bool maximize(theory_var v) { return max_min(v, true); }
+        virtual bool maximize(theory_var v);
         virtual theory_var add_objective(app* term);
         virtual inf_eps_rational<inf_rational> get_objective_value(theory_var v);
         inf_rational m_objective;
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index d50b1d505..26c272548 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -975,6 +975,13 @@ namespace smt {
         return internalize_term_core(term);
     }
 
+    template<typename Ext>
+    bool theory_arith<Ext>::maximize(theory_var v) {
+        bool r = max_min(v, true); 
+        return r || at_upper(v);
+    }
+
+
     template<typename Ext>
     inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) { 
         inf_eps_rational<inf_rational> val(m_objective);