diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h
index 65575965f..e0b415c03 100644
--- a/src/smt/network_flow.h
+++ b/src/smt/network_flow.h
@@ -144,9 +144,11 @@ namespace smt {
         graph                m_graph;
         scoped_ptr<spanning_tree_base> m_tree;
         scoped_ptr<pivot_rule_impl>    m_pivot;
-        vector<fin_numeral>  m_balances;     // Denote supply/demand b_i on node i
-        vector<numeral>      m_potentials;   // Duals of flows which are convenient to compute dual solutions        
-        vector<numeral>      m_flows;        // Basic feasible flows
+        vector<fin_numeral>  m_balances;     // nodes + 1 |-> [b -1b] Denote supply/demand b_i on node i
+        vector<numeral>      m_potentials;   // nodes + 1 |-> initial: +/- 1  
+                                             // Duals of flows which are convenient to compute dual solutions 
+                                             // become solutions to Dual simplex.
+        vector<numeral>      m_flows;        // edges + nodes |-> assignemnt Basic feasible flows
         svector<edge_state>  m_states;
         unsigned             m_step;
         edge_id              m_enter_id;
@@ -176,9 +178,10 @@ namespace smt {
         bool check_well_formed();
         bool check_optimal();
 
-        void display(std::ofstream & os);
+        void display_primal(std::ofstream & os);
         void display_dual(std::ofstream & os);
         void display_spanning_tree(std::ofstream & os);
+        void display_system(std::ofstream & os);
 
     public:
 
diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h
index 683ea0b98..777bd07a3 100644
--- a/src/smt/network_flow_def.h
+++ b/src/smt/network_flow_def.h
@@ -28,7 +28,7 @@ namespace smt {
 
     template<typename Ext>    
     bool network_flow<Ext>::first_eligible_pivot::choose_entering_edge() {
-        TRACE("network_flow", tout << "choose_entering_edge...\n";);        
+        numeral cost = numeral::zero();
         int num_edges = m_graph.get_num_edges();
         for (int i = m_next_edge; i < m_next_edge + num_edges; ++i) {
             edge_id id = i % num_edges;
@@ -37,65 +37,51 @@ namespace smt {
             }
             node src = m_graph.get_source(id);
             node tgt = m_graph.get_target(id);
-            numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
+            cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
             if (cost.is_pos()) {
                 m_next_edge = m_enter_id = id;
-                TRACE("network_flow", 
-                      tout << "Found entering edge " << id << " between node ";
-                      tout << src << " and node " << tgt << " with reduced cost = " << cost << "...\n";);
                 return true;
             }
         }
-        TRACE("network_flow", tout << "Found no entering edge...\n";);
         return false;
     };
 
     template<typename Ext>    
     bool network_flow<Ext>::best_eligible_pivot::choose_entering_edge() {
-        TRACE("network_flow", tout << "choose_entering_edge...\n";);        
         unsigned num_edges = m_graph.get_num_edges();
-        numeral max = numeral::zero();
+        numeral cost = numeral::zero();
         for (unsigned i = 0; i < num_edges; ++i) {
             node src = m_graph.get_source(i);
             node tgt = m_graph.get_target(i);
             if (!edge_in_tree(i)) {
-                numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(i);
-                if (cost > max) {
-                    max = cost;
+                numeral new_cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(i);
+                if (new_cost > cost) {
+                    cost = new_cost;
                     m_enter_id = i;
                 }
             }
         }
-        if (max.is_pos()) {
-            TRACE("network_flow", {
-                    tout << "Found entering edge " << m_enter_id << " between node ";
-                    tout << m_graph.get_source(m_enter_id) << " and node " << m_graph.get_target(m_enter_id);
-                    tout << " with reduced cost = " << max << "...\n";
-                });
-            return true;
-        }
-        TRACE("network_flow", tout << "Found no entering edge...\n";);
-        return false;
+        return cost.is_pos();
     };
 
     template<typename Ext>    
     bool network_flow<Ext>::candidate_list_pivot::choose_entering_edge() {
+        numeral cost = numeral::zero();
         if (m_current_length == 0 || m_minor_step == MINOR_STEP_LIMIT) {
             // Build the candidate list
             unsigned num_edges = m_graph.get_num_edges();
-            numeral max = numeral::zero();
             m_current_length = 0;
             for (unsigned i = m_next_edge; i < m_next_edge + num_edges; ++i) {
                 edge_id id = (i >= num_edges) ? i - num_edges : i;
                 node src = m_graph.get_source(id);
                 node tgt = m_graph.get_target(id);
                 if (!edge_in_tree(id)) {
-                    numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
-                    if (cost.is_pos()) {
+                    numeral new_cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
+                    if (new_cost.is_pos()) {
                         m_candidates[m_current_length] = id;
                         ++m_current_length;
-                        if (cost > max) {
-                            max = cost;
+                        if (new_cost > cost) {
+                            cost = new_cost;
                             m_enter_id = id;
                         }
                     }
@@ -104,48 +90,29 @@ namespace smt {
             }
             m_next_edge = m_enter_id;
             m_minor_step = 1;
-            if (max.is_pos()) {
-                TRACE("network_flow", {
-                        tout << "Found entering edge " << m_enter_id << " between node ";
-                        tout << m_graph.get_source(m_enter_id) << " and node " << m_graph.get_target(m_enter_id);
-                        tout << " with reduced cost = " << max << "...\n";
-                    });
-                return true;
-            }
-            TRACE("network_flow", tout << "Found no entering edge...\n";);
-            return false;
+            return cost.is_pos();
         }
         
         ++m_minor_step;
-        numeral max = numeral::zero();
         for (unsigned i = 0; i < m_current_length; ++i) {
             edge_id id = m_candidates[i];
             node src = m_graph.get_source(id);
             node tgt = m_graph.get_target(id);
             if (!edge_in_tree(id)) {
-                numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
-                if (cost > max) {
-                    max = cost;
+                numeral new_cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(id);
+                if (new_cost > cost) {
+                    cost = new_cost;
                     m_enter_id = id;
                 }
                 // Remove stale candidates
-                if (!cost.is_pos()) {
+                if (!new_cost.is_pos()) {
                     --m_current_length;
                     m_candidates[i] = m_candidates[m_current_length];
                     --i;
                 }
             }
         }
-        if (max.is_pos()) {
-            TRACE("network_flow", {
-                    tout << "Found entering edge " << m_enter_id << " between node ";
-                    tout << m_graph.get_source(m_enter_id) << " and node " << m_graph.get_target(m_enter_id);
-                    tout << " with reduced cost = " << max << "...\n";
-                });
-            return true;
-        }
-        TRACE("network_flow", tout << "Found no entering edge...\n";);
-        return false;
+        return cost.is_pos();
     };
 
     template<typename Ext>
@@ -167,7 +134,7 @@ namespace smt {
             tout << "Difference logic optimization:" << std::endl;
             display_dual(tout);
             tout << "Minimum cost flow:" << std::endl;
-            display(tout);
+            display_primal(tout);
             };);
 
         m_step = 0;
@@ -219,7 +186,8 @@ namespace smt {
               tout << pp_vector("Flows", m_flows);
               tout << "Cost: " << get_cost() << "\n";
               tout << "Spanning tree:\n";               
-              display_spanning_tree(tout););
+              display_spanning_tree(tout);
+              display_primal(tout););
         SASSERT(check_well_formed());
     }
 
@@ -252,7 +220,6 @@ namespace smt {
 
     template<typename Ext>
     void network_flow<Ext>::update_flows() {
-        TRACE("network_flow", tout << "update_flows...\n";);
         m_flows[m_enter_id] += *m_delta;
         node src = m_graph.get_source(m_enter_id);
         node tgt = m_graph.get_target(m_enter_id); 
@@ -269,7 +236,6 @@ namespace smt {
     
     template<typename Ext>
     bool network_flow<Ext>::choose_leaving_edge() {        
-        TRACE("network_flow", tout << "choose_leaving_edge...\n";);
         node src = m_graph.get_source(m_enter_id);
         node tgt = m_graph.get_target(m_enter_id); 
         m_delta.set_invalid();
@@ -286,14 +252,7 @@ namespace smt {
             }
         }
         m_leave_id = leave_id;
-        
-        TRACE("network_flow", 
-              tout << "Leaving edge " << m_leave_id;
-              tout << " between node " << m_graph.get_source(m_leave_id);
-              tout << " and node " << m_graph.get_target(m_leave_id) ;
-              if (m_delta) tout << " with delta = " << *m_delta;
-              tout << "\n";);            
-
+       
         return m_delta;
     }
 
@@ -329,6 +288,19 @@ namespace smt {
         while (choose_entering_edge(pr)) { 
             bool bounded = choose_leaving_edge();
             if (!bounded) return UNBOUNDED;
+            //TRACE("network_flow",
+                  {
+                      vector<edge>const& es = m_graph.get_all_edges();
+                      edge const& e_in = es[m_enter_id];
+                      edge const& e_out = es[m_leave_id];
+                      node src_in = e_in.get_source(), tgt_in = e_in.get_target();
+                      node src_out = e_out.get_source(), tgt_out = e_out.get_target();
+                      numeral c1 = m_potentials[src_in] - m_potentials[tgt_in] - m_graph.get_weight(m_enter_id);
+                      numeral c2 = m_potentials[src_out] - m_potentials[tgt_out] - m_graph.get_weight(m_leave_id);
+                      tout << "new base: y_" << src_in  << "_" << tgt_in  << " cost: " << c1 << " delta: " << *m_delta << "\n";
+                      tout << "old base: y_" << src_out << "_" << tgt_out << " cost: " << c2 << "\n";                  
+                  }
+              //    );
             update_flows();
             if (m_enter_id != m_leave_id) {
                 SASSERT(edge_in_tree(m_leave_id));
@@ -340,10 +312,18 @@ namespace smt {
                 TRACE("network_flow", 
                       tout << "Spanning tree:\n"; 
                       display_spanning_tree(tout);
-                      tout << "Cost: " << get_cost() << "\n";);
+                      tout << "Cost: " << get_cost() << "\n";
+                      display_primal(tout);
+                      );
                 SASSERT(check_well_formed());
             }
         }
+        TRACE("network_flow", 
+              tout << "Spanning tree:\n"; 
+              display_spanning_tree(tout);
+              tout << "Cost: " << get_cost() << "\n";
+              display_primal(tout);
+              );
         if (is_infeasible()) return INFEASIBLE;
         TRACE("network_flow", tout << "Found optimal solution.\n";);
         SASSERT(check_optimal());
@@ -352,14 +332,13 @@ namespace smt {
 
     template<typename Ext>
     bool network_flow<Ext>::is_infeasible() {
-#if 0
         // Flows of artificial arcs should be zero
         unsigned num_nodes = m_graph.get_num_nodes();
         unsigned num_edges = m_graph.get_num_edges();
+        SASSERT(m_flows.size() == num_edges);
         for (unsigned i = 1; i < num_nodes; ++i) {
             if (m_flows[num_edges - i].is_pos()) return true;
         }
-#endif
         return false;
     }
 
@@ -445,7 +424,7 @@ namespace smt {
     // display methods
 
     template<typename Ext>
-    void network_flow<Ext>::display(std::ofstream & os) {
+    void network_flow<Ext>::display_primal(std::ofstream & os) {
         vector<edge> const & es = m_graph.get_all_edges();
         for (unsigned i = 0; i < m_graph.get_num_edges(); ++i) {
             edge const & e = es[i];
@@ -486,6 +465,12 @@ namespace smt {
         };
         os << "))" << std::endl;
         os << "(optimize)" << std::endl;
+        if (!m_flows.empty()) {
+            for (unsigned i = 0; i < m_graph.get_num_edges(); ++i) {
+                edge const & e = es[i];
+                os << "; y_" << e.get_source() << "_" << e.get_target() << " = " << m_flows[i] << "\n";
+            }
+        }
     }
 
 
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index f6b704359..015144c2a 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -165,8 +165,7 @@ namespace smt {
         arith_eq_adapter               m_arith_eq_adapter;
         theory_diff_logic_statistics   m_stats;
         dl_graph<GExt>                 m_graph;
-        theory_var                     m_zero_int; // cache the variable representing the zero variable.
-        theory_var                     m_zero_real; // cache the variable representing the zero variable.
+        theory_var                     m_zero; // cache the variable representing the zero variable.
         int_vector                     m_scc_id;                  // Cheap equality propagation
         eq_prop_info_set               m_eq_prop_info_set;        // set of existing equality prop infos
         ptr_vector<eq_prop_info>       m_eq_prop_infos;
@@ -217,8 +216,7 @@ namespace smt {
             m_params(params),
             m_util(m),
             m_arith_eq_adapter(*this, params, m_util),
-            m_zero_int(null_theory_var),
-            m_zero_real(null_theory_var),
+            m_zero(null_theory_var),
             m_asserted_qhead(0),
             m_num_core_conflicts(0),
             m_num_propagation_calls(0),
@@ -358,9 +356,9 @@ namespace smt {
 
         void get_implied_bound_antecedents(edge_id bridge_edge, edge_id subsumed_edge, conflict_resolution & cr);
 
-        theory_var get_zero(sort* s) const { return m_util.is_int(s)?m_zero_int:m_zero_real; }
+        theory_var get_zero(sort* s) const { return m_zero; }
 
-        theory_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
+        theory_var get_zero(expr* e) const { return m_zero; }
 
         void inc_conflicts();
 
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 7472edd8b..4202b86a3 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -71,12 +71,7 @@ void theory_diff_logic<Ext>::init(context * ctx) {
     zero = m_util.mk_numeral(rational(0), true);
     e = ctx->mk_enode(zero, false, false, true);
     SASSERT(!is_attached_to_var(e));
-    m_zero_int = mk_var(e);
-
-    zero = m_util.mk_numeral(rational(0), false);
-    e = ctx->mk_enode(zero, false, false, true);
-    SASSERT(!is_attached_to_var(e));
-    m_zero_real = mk_var(e);
+    m_zero = mk_var(e);
 }
 
 
@@ -356,7 +351,7 @@ final_check_status theory_diff_logic<Ext>::final_check_eh() {
 
     TRACE("arith_final", display(tout); );
     // either will already be zero (as we don't do mixed constraints).
-    m_graph.set_to_zero(m_zero_int, m_zero_real);
+    m_graph.set_to_zero(m_zero);
     SASSERT(is_consistent());
     if (m_non_diff_logic_exprs) {
         return FC_GIVEUP; 
@@ -766,8 +761,7 @@ void theory_diff_logic<Ext>::reset_eh() {
         dealloc(m_atoms[i]);
     }
     m_graph            .reset();
-    m_zero_int          = null_theory_var;
-    m_zero_real         = null_theory_var;
+    m_zero              = null_theory_var;
     m_atoms            .reset();
     m_asserted_atoms   .reset();
     m_stats            .reset();
@@ -1022,10 +1016,9 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
         sum += balance;
     }    
     // HACK: assume that v0 is always value 0
-    if (balances[0].is_zero()) {
-        balances[0] = -sum;
-    }
+    balances[0] = -sum;
 
+    TRACE("arith", display(tout););
     network_flow<GExt> net_flow(m_graph, balances);
     min_flow_result result = net_flow.min_cost();
     SASSERT(result != UNBOUNDED);
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 4a5d97d52..5358fb758 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -138,8 +138,7 @@ namespace smt {
         smt_params              m_params;
         arith_util              a;
         arith_eq_adapter        m_arith_eq_adapter;
-        th_var                  m_zero_int; // cache the variable representing the zero variable.
-        th_var                  m_zero_real; // cache the variable representing the zero variable.
+        th_var                  m_zero; //cache the variable representing the zero variable.
 
         dl_graph<GExt>          m_graph;
         nc_functor              m_nc_functor;
@@ -304,7 +303,7 @@ namespace smt {
 
         void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
         
-        th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; }
+        th_var get_zero(sort* s) const { return m_zero; }
 
         th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); }
 
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 6039b208a..e6ec7e387 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -62,8 +62,7 @@ namespace smt {
             theory(m.mk_family_id("arith")),
             a(m),
             m_arith_eq_adapter(*this, m_params, a),
-            m_zero_int(null_theory_var),
-            m_zero_real(null_theory_var),
+            m_zero(null_theory_var),
             m_nc_functor(*this),
             m_asserted_qhead(0),
             m_agility(0.5),
@@ -134,8 +133,7 @@ namespace smt {
     template<typename Ext>
     void theory_utvpi<Ext>::reset_eh() {
         m_graph            .reset();
-        m_zero_int          = null_theory_var;
-        m_zero_real         = null_theory_var;
+        m_zero              = null_theory_var;
         m_atoms            .reset();
         m_asserted_atoms   .reset();
         m_stats            .reset();
@@ -261,8 +259,7 @@ namespace smt {
     template<typename Ext>
     void theory_utvpi<Ext>::init(context* ctx) {
         theory::init(ctx);
-        m_zero_int  = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true));
-        m_zero_real = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), false), false, false, true));
+        m_zero  = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true));
     }
 
     /**
@@ -556,7 +553,7 @@ namespace smt {
         theory_var v = null_theory_var;
         context& ctx = get_context();
         if (r.is_zero()) {            
-            v = a.is_int(n)?m_zero_int:m_zero_real;
+            v = m_zero;
         }
         else if (ctx.e_internalized(n)) {
             enode* e = ctx.get_enode(n);
@@ -778,9 +775,7 @@ namespace smt {
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
         enforce_parity();
-        m_graph.set_to_zero(to_var(m_zero_int), to_var(m_zero_real));
-        m_graph.set_to_zero(neg(to_var(m_zero_int)), neg(to_var(m_zero_real)));
-        m_graph.set_to_zero(to_var(m_zero_int), neg(to_var(m_zero_int)));
+        m_graph.set_to_zero(to_var(m_zero), neg(to_var(m_zero)));
         compute_delta();   
         DEBUG_CODE(validate_model(););
     }