diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index fd4e52b17..beae83fe0 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -27,7 +27,7 @@ Notes:
 
 #include "ast.h"
 #include "solver.h"
-#include "optimize_objectives.h"
+#include "optsmt.h"
 #include "opt_maxsmt.h"
 
 namespace opt {
@@ -39,7 +39,7 @@ namespace opt {
         expr_ref_vector     m_hard_constraints;
         ref<solver>         m_solver;
         params_ref          m_params;
-        optimize_objectives m_optsmt;
+        optsmt              m_optsmt;
         maxsmt              m_maxsmt;
     public:
         context(ast_manager& m);
diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optsmt.cpp
similarity index 92%
rename from src/opt/optimize_objectives.cpp
rename to src/opt/optsmt.cpp
index 663f3a52c..4dcefb577 100644
--- a/src/opt/optimize_objectives.cpp
+++ b/src/opt/optsmt.cpp
@@ -3,7 +3,7 @@ Copyright (c) 2013 Microsoft Corporation
 
 Module Name:
 
-    optimize_objectives.cpp
+    optsmt.cpp
 
 Abstract:
    
@@ -40,7 +40,7 @@ Notes:
 #ifndef _OPT_OBJECTIVE_H_
 #define _OPT_OBJECTIVE_H_
 
-#include "optimize_objectives.h"
+#include "optsmt.h"
 #include "opt_solver.h"
 #include "arith_decl_plugin.h"
 #include "theory_arith.h"
@@ -51,11 +51,11 @@ Notes:
 namespace opt {
 
 
-    void optimize_objectives::set_cancel(bool f) {
+    void optsmt::set_cancel(bool f) {
         m_cancel = true;
     }
 
-    void optimize_objectives::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src) {
+    void optsmt::set_max(vector<inf_eps>& dst, vector<inf_eps> const& src) {
         for (unsigned i = 0; i < src.size(); ++i) {
             if (src[i] > dst[i]) {
                 dst[i] = src[i];
@@ -66,7 +66,7 @@ namespace opt {
     /*
         Enumerate locally optimal assignments until fixedpoint.
     */
-    lbool optimize_objectives::basic_opt() {
+    lbool optsmt::basic_opt() {
         opt_solver::toggle_objective _t(*s, true);          
         lbool is_sat = l_true;
 
@@ -86,7 +86,7 @@ namespace opt {
     /*
         Enumerate locally optimal assignments until fixedpoint.
     */
-    lbool optimize_objectives::farkas_opt() {
+    lbool optsmt::farkas_opt() {
         smt::theory_opt& opt = s->get_optimizer();
 
         IF_VERBOSE(1, verbose_stream() << typeid(opt).name() << "\n";);
@@ -107,7 +107,7 @@ namespace opt {
         return l_true;        
     }
 
-    void optimize_objectives::update_lower() {
+    void optsmt::update_lower() {
         model_ref md;
         s->get_model(md);
         set_max(m_lower, s->get_objective_values());
@@ -129,7 +129,7 @@ namespace opt {
         s->assert_expr(constraint);
     }
 
-    lbool optimize_objectives::update_upper() {
+    lbool optsmt::update_upper() {
         smt::theory_opt& opt = s->get_optimizer();
 
         SASSERT(typeid(smt::theory_inf_arith) == typeid(opt));
@@ -205,7 +205,7 @@ namespace opt {
        Takes solver with hard constraints added.
        Returns an optimal assignment to objective functions.
     */
-    lbool optimize_objectives::operator()(opt_solver& solver) {
+    lbool optsmt::operator()(opt_solver& solver) {
         s = &solver;
         s->reset_objectives();
         m_lower.reset();
@@ -245,7 +245,7 @@ namespace opt {
         return is_sat;
     }
 
-    inf_eps  optimize_objectives::get_value(bool as_positive, unsigned index) const {
+    inf_eps  optsmt::get_value(bool as_positive, unsigned index) const {
         if (as_positive) {
             return m_lower[index];
         }
@@ -254,7 +254,7 @@ namespace opt {
         }
     }
 
-    void optimize_objectives::display(std::ostream& out) const {
+    void optsmt::display(std::ostream& out) const {
         unsigned sz = m_objs.size();
         for (unsigned i = 0; i < sz; ++i) {
             bool is_max = m_is_max[i];
@@ -270,7 +270,7 @@ namespace opt {
         }        
     }
 
-    void optimize_objectives::add(app* t, bool is_max) {
+    void optsmt::add(app* t, bool is_max) {
         expr_ref t1(t, m), t2(m);
         th_rewriter rw(m);
         if (!is_max) {
diff --git a/src/opt/optimize_objectives.h b/src/opt/optsmt.h
similarity index 89%
rename from src/opt/optimize_objectives.h
rename to src/opt/optsmt.h
index 6519bb42f..1d51dadfc 100644
--- a/src/opt/optimize_objectives.h
+++ b/src/opt/optsmt.h
@@ -3,7 +3,7 @@ Copyright (c) 2013 Microsoft Corporation
 
 Module Name:
 
-    optimize_objectives.h
+    optsmt.h
 
 Abstract:
    
@@ -27,7 +27,7 @@ namespace opt {
        Returns an optimal assignment to objective functions.
     */
 
-    class optimize_objectives {
+    class optsmt {
         ast_manager&     m;
         opt_solver*      s;
         volatile bool    m_cancel;
@@ -38,7 +38,7 @@ namespace opt {
         svector<smt::theory_var> m_vars;
         symbol m_engine;
     public:
-        optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false), m_objs(m) {}
+        optsmt(ast_manager& m): m(m), s(0), m_cancel(false), m_objs(m) {}
 
         lbool operator()(opt_solver& s);