diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp
index ffba96a9e..8e76a2914 100644
--- a/src/opt/optimize_objectives.cpp
+++ b/src/opt/optimize_objectives.cpp
@@ -43,7 +43,7 @@ Notes:
 #include "optimize_objectives.h"
 #include "opt_solver.h"
 #include "arith_decl_plugin.h"
-#include "smt_context.h"
+#include "theory_arith.h"
 
 namespace opt {
 
@@ -115,6 +115,7 @@ namespace opt {
     }
 
     lbool optimize_objectives::update_upper() {
+        NOT_IMPLEMENTED_YET();
         return l_undef;
     }
 
diff --git a/src/smt/theory_arith.cpp b/src/smt/theory_arith.cpp
index 6c18b66c3..9a7d08151 100644
--- a/src/smt/theory_arith.cpp
+++ b/src/smt/theory_arith.cpp
@@ -26,5 +26,5 @@ namespace smt {
     // template class theory_arith<si_ext>;
     // template class theory_arith<smi_ext>;
 
-    // TBD: template class smt::theory_arith<inf_ext>;    
+    template class smt::theory_arith<inf_ext>;    
 };
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 80731ab1d..75a0f9ff3 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -432,7 +432,7 @@ namespace smt {
         bool                    m_eager_gcd; // true if gcd should be applied at every add_row
         unsigned                m_final_check_idx;
 
-        inf_rational            m_objective_value;
+        inf_eps_rational<inf_rational>   m_objective_value;
 
         // backtracking
         svector<bound_trail>    m_bound_trail;
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index d43d1ef24..a1fff392f 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -999,7 +999,7 @@ namespace smt {
 
     template<typename Ext>
     inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) {
-        return inf_eps_rational<inf_rational>(m_objective_value); 
+        return m_objective_value; 
     }
 
     /**
diff --git a/src/util/inf_eps_rational.h b/src/util/inf_eps_rational.h
index a8d32e2b2..d7fdaf4fc 100644
--- a/src/util/inf_eps_rational.h
+++ b/src/util/inf_eps_rational.h
@@ -143,15 +143,15 @@ class inf_eps_rational {
         return m_infty;
     }
 
-    static const inf_eps_rational & zero() {
+    static inf_eps_rational zero() {
         return inf_eps_rational(Numeral::zero());
     }
 
-    static const inf_eps_rational & one() {
+    static inf_eps_rational one() {
         return inf_eps_rational(Numeral::one());
     }
 
-    static const inf_eps_rational & minus_one() {
+    static inf_eps_rational minus_one() {
         return inf_eps_rational(Numeral::minus_one());
     }