diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index de4156747..695b53395 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -82,6 +82,10 @@ namespace opt {
 
     unsigned context::add_objective(app* t, bool is_max) {
         app_ref tr(t, m);
+        arith_util a(m);
+        if (!a.is_arith_expr(t)) {
+            throw default_exception("Objective must be integer or real");   
+        }
         unsigned index = m_objectives.size();
         m_objectives.push_back(objective(is_max, tr, index));
         return index;
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 29cef424d..7b23161d6 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -261,10 +261,14 @@ namespace opt {
     }
 
     
-    void opt_solver::to_smt2_benchmark(std::ofstream & buffer, 
-                                       unsigned num_assumptions, expr * const * assumptions,
-                                       char const * name, char const * logic, 
-                                       char const * status, char const * attributes) {        
+    void opt_solver::to_smt2_benchmark(
+        std::ofstream & buffer, 
+        unsigned num_assumptions, 
+        expr * const * assumptions,
+        char const * name, 
+        char const * logic, 
+        char const * status, 
+        char const * attributes) {        
         ast_smt_pp pp(m);
         pp.set_benchmark_name(name);
         pp.set_logic(logic);