diff --git a/src/opt/objective_decl_plugin.cpp b/src/opt/objective_decl_plugin.cpp
index b02ceee27..9bca883ff 100644
--- a/src/opt/objective_decl_plugin.cpp
+++ b/src/opt/objective_decl_plugin.cpp
@@ -48,6 +48,7 @@ namespace opt{
         SASSERT(num_parameters == 0);
         symbol name = get_name(static_cast<obj_kind>(k));
         func_decl_info info(get_family_id(), k, num_parameters, parameters);
+        range = mk_sort(OBJECTIVE_SORT, 0, 0);
         return m_manager->mk_func_decl(name, arity, domain, range, info);
     }
     
diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp
index 8cf432e7b..35e6ff9f0 100644
--- a/src/opt/opt_cmds.cpp
+++ b/src/opt/opt_cmds.cpp
@@ -80,9 +80,6 @@ public:
     }
 
     virtual void reset(cmd_context & ctx) { 
-        if (m_formula) {
-            ctx.m().dec_ref(m_formula);
-        }
         m_idx = 0; 
         m_formula = 0;
         m_id = symbol::null;
@@ -116,7 +113,6 @@ public:
             throw cmd_exception("Invalid type for expression. Expected Boolean type.");
         }
         m_formula = t;
-        ctx.m().inc_ref(t);
         ++m_idx;
     }
 
@@ -298,9 +294,6 @@ public:
         reset(ctx);
     }
     virtual void reset(cmd_context& ctx) {
-        if (m_objective) {
-            ctx.m().dec_ref(m_objective);
-        }
         m_objective = 0;
         m_idx = 0;
     }
@@ -312,7 +305,6 @@ public:
 
     virtual void set_next_arg(cmd_context & ctx, expr * arg) {
         m_objective = arg;
-        ctx.m().inc_ref(arg);
         ++m_idx;
     }