diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h
index 86429b1a2..9685af589 100644
--- a/src/math/simplex/simplex.h
+++ b/src/math/simplex/simplex.h
@@ -142,6 +142,7 @@ namespace simplex {
         void  set_value(var_t var, eps_numeral const& b);        
         void  set_cancel(bool f) { m_cancel = f; }
         void  set_max_iterations(unsigned m) { m_max_iterations = m; }
+        void  reset();
         lbool make_feasible();
         lbool minimize(var_t var);
         eps_numeral const& get_value(var_t v);
diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h
index daa718472..3c1a90a7a 100644
--- a/src/math/simplex/simplex_def.h
+++ b/src/math/simplex/simplex_def.h
@@ -310,6 +310,16 @@ namespace simplex {
         }
     }
 
+    template<typename Ext>
+    void simplex<Ext>::reset() {
+        M.reset();
+        m_to_patch.reset();
+        m_vars.reset();
+        m_row2base.reset();
+        m_left_basis.reset();
+        m_base_vars.reset();
+    }
+
     template<typename Ext>
     lbool simplex<Ext>::make_feasible() {
         ++m_stats.m_num_checks;
diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h
index 1c9f0fde8..80454a52c 100644
--- a/src/math/simplex/sparse_matrix.h
+++ b/src/math/simplex/sparse_matrix.h
@@ -145,6 +145,7 @@ namespace simplex {
 
         sparse_matrix(manager& m): m(m) {}
         ~sparse_matrix();
+        void reset();
         
         class row {
             unsigned m_id;            
diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h
index f4c25658e..9fa3ceda7 100644
--- a/src/math/simplex/sparse_matrix_def.h
+++ b/src/math/simplex/sparse_matrix_def.h
@@ -280,6 +280,16 @@ namespace simplex {
         }
     }
 
+    template<typename Ext>
+    void sparse_matrix<Ext>::reset() {
+        m_rows.reset();
+        m_dead_rows.reset();
+        m_columns.reset();
+        m_var_pos.reset();
+        m_var_pos_idx.reset();
+
+    }
+
     template<typename Ext>
     void sparse_matrix<Ext>::ensure_var(var_t v) {
         while (m_columns.size() <= v) {
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index e09b4f91e..27a2d3e58 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -38,6 +38,8 @@ Revision History:
 #include"numeral_factory.h"
 #include"smt_clause.h"
 #include"theory_opt.h"
+#include"simplex.h"
+#include"simplex_def.h"
 
 // The DL theory can represent term such as n + k, where n is an enode and k is a numeral.
 namespace smt {
@@ -62,6 +64,7 @@ namespace smt {
     class theory_diff_logic : public theory, public theory_opt, private Ext {
         
         typedef typename Ext::numeral numeral;
+        typedef simplex::simplex<simplex::mpq_ext> Simplex;
 
         class atom {
             bool_var  m_bvar;
@@ -194,6 +197,9 @@ namespace smt {
         vector<objective_term>         m_objectives;
         vector<rational>               m_objective_consts;
         vector<expr_ref_vector>        m_objective_assignments;
+        vector<Simplex::row>           m_objective_rows;
+        Simplex                        m_S;
+        unsigned                       m_num_simplex_edges;
 
         // Set a conflict due to a negative cycle.
         void set_neg_cycle_conflict();
@@ -228,7 +234,8 @@ namespace smt {
             m_is_lia(true),
             m_non_diff_logic_exprs(false),
             m_factory(0),
-            m_nc_functor(*this) {
+            m_nc_functor(*this),
+            m_num_simplex_edges(0) {
         }            
 
         virtual ~theory_diff_logic() {
@@ -369,6 +376,15 @@ namespace smt {
 
         void inc_conflicts();
 
+        // Optimization:
+        // convert variables, edges and objectives to simplex.
+        unsigned node2simplex(unsigned v);
+        unsigned edge2simplex(unsigned e);
+        unsigned obj2simplex(unsigned v);
+        unsigned num_simplex_vars();
+        bool is_simplex_edge(unsigned e);
+        unsigned simplex2edge(unsigned e);
+        void update_simplex(Simplex& S);
     };
 
     struct idl_ext {
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index d7bc45374..7189ee219 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -29,8 +29,6 @@ Revision History:
 #include"warning.h"
 #include"smt_model_generator.h"
 #include"model_implicant.h"
-#include"simplex.h"
-#include"simplex_def.h"
 
 
 using namespace smt;
@@ -343,7 +341,13 @@ void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) {
     m_asserted_atoms.shrink(s.m_asserted_atoms_lim);
     m_asserted_qhead = s.m_asserted_qhead_old;
     m_scopes.shrink(new_lvl);
+    unsigned num_edges = m_graph.get_num_edges();
     m_graph.pop(num_scopes);
+    if (num_edges != m_graph.get_num_edges() && m_num_simplex_edges > 0) {
+        m_S.reset();
+        m_num_simplex_edges = 0;
+        m_objective_rows.reset();
+    }
     theory::pop_scope_eh(num_scopes);
 }
 
@@ -1066,12 +1070,120 @@ void theory_diff_logic<Ext>::get_implied_bound_antecedents(edge_id bridge_edge,
     m_graph.explain_subsumed_lazy(bridge_edge, subsumed_edge, f);
 }
 
+template<typename Ext>
+unsigned theory_diff_logic<Ext>::node2simplex(unsigned v) {
+    //return v;
+    return m_objectives.size() + 2*v + 1;
+}
+template<typename Ext>
+unsigned theory_diff_logic<Ext>::edge2simplex(unsigned e) {
+    //return m_graph.get_num_nodes() + e;
+    return m_objectives.size() + 2*e;
+}
+template<typename Ext>
+unsigned theory_diff_logic<Ext>::obj2simplex(unsigned e) {
+    //return m_graph.get_num_nodes() + m_graph.get_num_edges() + e;
+    return e;
+}
+
+template<typename Ext>
+unsigned theory_diff_logic<Ext>::num_simplex_vars() {
+    //return m_graph.get_num_nodes() + m_graph.get_num_edges() + m_objectives.size();
+    return m_objectives.size() + std::max(2*m_graph.get_num_edges(),2*m_graph.get_num_nodes()+1);
+}
+
+template<typename Ext>
+bool theory_diff_logic<Ext>::is_simplex_edge(unsigned e) {
+#if 0
+    return 
+        m_graph.get_num_nodes() <= e &&
+        e < m_graph.get_num_nodes() + m_graph.get_num_edges();
+#else
+    if (e < m_objectives.size()) return false;
+    e -= m_objectives.size();
+    return (0 == (e & 0x1));
+#endif
+}
+
+template<typename Ext> 
+unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
+    SASSERT(is_simplex_edge(e));
+    //return e - m_graph.get_num_nodes();
+    return (e - m_objectives.size())/2;
+}
+
+template<typename Ext> 
+void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
+    unsigned num_nodes = m_graph.get_num_nodes();
+    vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
+    S.ensure_var(num_simplex_vars());
+    for (unsigned i = 0; i < num_nodes; ++i) {
+        numeral const& a = m_graph.get_assignment(i);
+        rational fin = a.get_rational().to_rational();
+        rational inf = a.get_infinitesimal().to_rational();
+        mpq_inf q(fin.to_mpq(), inf.to_mpq());
+        S.set_value(node2simplex(i), q);
+    }
+    S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
+    S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
+    svector<unsigned> vars;
+    unsynch_mpq_manager mgr;
+    scoped_mpq_vector coeffs(mgr);
+    coeffs.push_back(mpq(1));
+    coeffs.push_back(mpq(-1));
+    coeffs.push_back(mpq(-1));
+    vars.resize(3);
+    for (unsigned i = m_num_simplex_edges; i < es.size(); ++i) {
+        //    t - s <= w 
+        // =>
+        //    t - s - b = 0, b >= w
+        dl_edge<GExt> const& e = es[i];
+        unsigned base_var = edge2simplex(i);
+        vars[0] = node2simplex(e.get_target());
+        vars[1] = node2simplex(e.get_source());
+        vars[2] = base_var;
+        S.add_row(base_var, 3, vars.c_ptr(), coeffs.c_ptr());        
+    }
+    m_num_simplex_edges = es.size();
+    for (unsigned i = 0; i < es.size(); ++i) {
+        dl_edge<GExt> const& e = es[i];
+        unsigned base_var = edge2simplex(i);
+        if (e.is_enabled()) {
+            numeral const& w = e.get_weight();
+            rational fin = w.get_rational().to_rational();
+            rational inf = w.get_infinitesimal().to_rational();
+            mpq_inf q(fin.to_mpq(),inf.to_mpq());
+            S.set_upper(base_var, q);
+        }
+        else {
+            S.unset_upper(base_var);
+        }
+    }
+    for (unsigned v = m_objective_rows.size(); v < m_objectives.size(); ++v) {
+        unsigned w = obj2simplex(v);
+        objective_term const& objective = m_objectives[v];
+
+        // add objective function as row.
+        coeffs.reset();
+        vars.reset();
+        for (unsigned i = 0; i < objective.size(); ++i) {
+            coeffs.push_back(objective[i].second.to_mpq());
+            vars.push_back(node2simplex(objective[i].first));
+        }
+        coeffs.push_back(mpq(1));
+        vars.push_back(w);
+        Simplex::row row = S.add_row(w, vars.size(), vars.c_ptr(), coeffs.c_ptr());
+        m_objective_rows.push_back(row);
+    }
+}
+
 template<typename Ext>
 inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker) {
     
-    typedef simplex::simplex<simplex::mpq_ext> Simplex;
-    Simplex S;
+    Simplex& S = m_S;
     ast_manager& m = get_manager();
+
+    update_simplex(S);
     objective_term const& objective = m_objectives[v];
 
     TRACE("arith",
@@ -1081,55 +1193,6 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, ex
           }
           tout << "Free coefficient " << m_objective_consts[v] << "\n";
           );
-    unsigned num_nodes = m_graph.get_num_nodes();
-    unsigned num_edges = m_graph.get_num_edges();
-    vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
-    S.ensure_var(num_nodes + num_edges + m_objectives.size());
-    for (unsigned i = 0; i < num_nodes; ++i) {
-        numeral const& a = m_graph.get_assignment(i);
-        rational fin = a.get_rational().to_rational();
-        rational inf = a.get_infinitesimal().to_rational();
-        mpq_inf q(fin.to_mpq(), inf.to_mpq());
-        S.set_value(i, q);
-    }
-    S.set_lower(get_zero(), mpq_inf(mpq(0), mpq(0)));
-    S.set_upper(get_zero(), mpq_inf(mpq(0), mpq(0)));
-    svector<unsigned> vars;
-    unsynch_mpq_manager mgr;
-    scoped_mpq_vector coeffs(mgr);
-    coeffs.push_back(mpq(1));
-    coeffs.push_back(mpq(-1));
-    coeffs.push_back(mpq(-1));
-    vars.resize(3);
-    for (unsigned i = 0; i < es.size(); ++i) {
-        dl_edge<GExt> const& e = es[i];
-        if (e.is_enabled()) {
-            unsigned base_var = num_nodes + i;
-            vars[0] = e.get_target();
-            vars[1] = e.get_source();
-            vars[2] = base_var;
-            S.add_row(base_var, 3, vars.c_ptr(), coeffs.c_ptr());
-            // t - s <= w
-            // t - s - b = 0, b >= w
-            numeral const& w = e.get_weight();
-            rational fin = w.get_rational().to_rational();
-            rational inf = w.get_infinitesimal().to_rational();
-            mpq_inf q(fin.to_mpq(),inf.to_mpq());
-            S.set_upper(base_var, q);
-        }
-    }
-    unsigned w = num_nodes + num_edges + v;
-
-    // add objective function as row.
-    coeffs.reset();
-    vars.reset();
-    for (unsigned i = 0; i < objective.size(); ++i) {
-        coeffs.push_back(objective[i].second.to_mpq());
-        vars.push_back(objective[i].first);
-    }
-    coeffs.push_back(mpq(1));
-    vars.push_back(w);
-    Simplex::row row = S.add_row(w, vars.size(), vars.c_ptr(), coeffs.c_ptr());
 
     TRACE("opt", S.display(tout); display(tout););
     
@@ -1141,11 +1204,13 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, ex
     }
     TRACE("opt", S.display(tout); );    
     SASSERT(is_sat != l_false);
+    unsigned w = obj2simplex(v);
     lbool is_fin = S.minimize(w);
     switch (is_fin) {
     case l_true: {
         simplex::mpq_ext::eps_numeral const& val = S.get_value(w);
         inf_rational r(-rational(val.first), -rational(val.second));
+        Simplex::row row = m_objective_rows[v];
         TRACE("opt", tout << r << " " << "\n"; 
               S.display_row(tout, row, true););
         Simplex::row_iterator it = S.row_begin(row), end = S.row_end(row);
@@ -1154,8 +1219,8 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, ex
         core.reset();
         for (; it != end; ++it) {
             unsigned v = it->m_var;
-            if (num_nodes <= v && v < num_nodes + num_edges) {
-                unsigned edge_id = v - num_nodes;
+            if (is_simplex_edge(v)) {
+                unsigned edge_id = simplex2edge(v);
                 literal lit = m_graph.get_explanation(edge_id);
                 get_context().literal2expr(lit, tmp);
                 core.push_back(tmp);