diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index 7899ef8da..89bc667e5 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -315,7 +315,7 @@ private:
         typename assignment_stack::iterator begin = m_assignment_stack.begin();
         while (it != begin) {
             --it;
-            TRACE("diff_logic_bug", tout << "undo assignment: " << it->get_var() << " " << it->get_old_value() << "\n";);
+            TRACE("dl_bug", tout << "undo assignment: " << it->get_var() << " " << it->get_old_value() << "\n";);
             m_assignment[it->get_var()] = it->get_old_value();
         }
         m_assignment_stack.reset();
@@ -371,7 +371,7 @@ private:
         SASSERT(m_gamma[target].is_neg());
         acc_assignment(target, gamma);
 
-        TRACE("arith", tout << id << "\n";);
+        TRACE("arith", display(tout << id << "\n"););
 
         dl_var source = target;
         while (true) {
@@ -467,7 +467,7 @@ public:
     // The graph does not have control over the ids assigned by the theory.
     // That is init_var receives the id as an argument.
     void init_var(dl_var v) {
-        TRACE("diff_logic_bug", tout << "init_var " << v << "\n";);
+        TRACE("dl_bug", tout << "init_var " << v << "\n";);
         if (static_cast<unsigned>(v) < m_out_edges.size() && (!m_out_edges[v].empty() || !m_in_edges[v].empty())) {
             return;
         }
@@ -485,7 +485,7 @@ public:
         }
         m_assignment[v].reset();
         SASSERT(static_cast<unsigned>(v) < m_heap.get_bounds());
-        TRACE("diff_logic_bug", tout << "init_var " << v << ", m_assignment[v]: " << m_assignment[v] << "\n";);
+        TRACE("dl_bug", tout << "init_var " << v << ", m_assignment[v]: " << m_assignment[v] << "\n";);
         SASSERT(m_assignment[v].is_zero());
         SASSERT(m_out_edges[v].empty());
         SASSERT(m_in_edges[v].empty());
@@ -934,7 +934,7 @@ private:
     // m_assignment[v] += inc
     // This method also stores the old value of v in the assignment stack.
     void acc_assignment(dl_var v, const numeral & inc) {
-        TRACE("diff_logic_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";);
+        TRACE("dl_bug", tout << "update v: " << v << " += " << inc << " m_assignment[v] " << m_assignment[v] << "\n";);
         m_assignment_stack.push_back(assignment_trail(v, m_assignment[v]));
         m_assignment[v] += inc;
     }
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 8fb244905..3dee2aa3d 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -377,7 +377,7 @@ namespace smt {
 
         void init_zero();
 
-        theory_var get_zero(bool is_int) { init_zero(); return is_int ? m_izero : m_rzero; }
+        theory_var get_zero(bool is_int) { return is_int ? m_izero : m_rzero; }
 
         void inc_conflicts();
 
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index d044c40ad..5e21792f6 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -66,6 +66,7 @@ void theory_diff_logic<Ext>::nc_functor::reset() {
 template<typename Ext>
 void theory_diff_logic<Ext>::init(context * ctx) {
     theory::init(ctx);
+    init_zero();
 }
 
 
@@ -192,10 +193,10 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
         found_non_diff_logic_expr(n);        
         return false;
     }
-	SASSERT(m_signs.size() == m_terms.size());
+    SASSERT(m_signs.size() == m_terms.size());
     if (m_terms.size() == 2 && m_signs[0] != m_signs[1]) {
-		app* a = m_terms.get(0), *b = m_terms.get(1);
-		bool sign0 = m_signs[0];
+        app* a = m_terms.get(0), *b = m_terms.get(1);
+        bool sign0 = m_signs[0];
         target = mk_var(a);
         source = mk_var(b);
         if (!sign0) {
@@ -212,7 +213,7 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
         k.neg();
     }
 
-	if (ctx.b_internalized(n)) return true;
+    if (ctx.b_internalized(n)) return true;
     bv = ctx.mk_bool_var(n);
     ctx.set_var_theory(bv, get_id());
     literal l(bv);
@@ -318,7 +319,7 @@ void theory_diff_logic<Ext>::collect_statistics(::statistics & st) const {
 
 template<typename Ext>
 void theory_diff_logic<Ext>::push_scope_eh() {
-
+    TRACE("arith", tout << "push\n";);
     theory::push_scope_eh();
     m_graph.push();
     m_scopes.push_back(scope());
@@ -330,6 +331,7 @@ void theory_diff_logic<Ext>::push_scope_eh() {
 
 template<typename Ext>
 void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) {
+    TRACE("arith", tout << "pop " << num_scopes << "\n";);
     unsigned lvl     = m_scopes.size();
     SASSERT(num_scopes <= lvl);
     unsigned new_lvl = lvl - num_scopes;
@@ -803,9 +805,9 @@ theory_var theory_diff_logic<Ext>::mk_var(app* n) {
     context & ctx = get_context();
     enode* e = nullptr;
     theory_var v = null_theory_var;
-	if (!ctx.e_internalized(n)) {
-		ctx.internalize(n, false);
-	}
+    if (!ctx.e_internalized(n)) {
+        ctx.internalize(n, false);
+    }
     e = ctx.get_enode(n);
     v = e->get_th_var(get_id());
 
@@ -1154,9 +1156,9 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
         // 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));
+        for (auto const& o : objective) {
+            coeffs.push_back(o.second.to_mpq());
+            vars.push_back(node2simplex(o.first));
         }
         coeffs.push_back(mpq(1));
         vars.push_back(w);
@@ -1169,11 +1171,11 @@ template<typename Ext>
 typename theory_diff_logic<Ext>::inf_eps theory_diff_logic<Ext>::value(theory_var v) {
      objective_term const& objective = m_objectives[v];   
      inf_eps r = inf_eps(m_objective_consts[v]);
-     for (unsigned i = 0; i < objective.size(); ++i) {
+     for (auto const& o : objective) {
          numeral n = m_graph.get_assignment(v);
          rational r1 = n.get_rational().to_rational();
          rational r2 = n.get_infinitesimal().to_rational();
-         r += objective[i].second * inf_eps(rational(0), inf_rational(r1, r2));
+         r += o.second * inf_eps(rational(0), inf_rational(r1, r2));
      }
      return r;
 }
@@ -1190,9 +1192,9 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
 
     TRACE("arith",
           objective_term const& objective = m_objectives[v];
-          for (unsigned i = 0; i < objective.size(); ++i) {
-              tout << "Coefficient " << objective[i].second 
-                   << " of theory_var " << objective[i].first << "\n";
+          for (auto const& o : objective) {
+              tout << "Coefficient " << o.second 
+                   << " of theory_var " << o.first << "\n";
           }
           tout << "Free coefficient " << m_objective_consts[v] << "\n";
           );
@@ -1385,6 +1387,7 @@ theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
 template<typename Ext>
 void theory_diff_logic<Ext>::init_zero() {
     if (m_izero != null_theory_var) return;
+    TRACE("arith", tout << "init zero\n";);
     context & ctx = get_context();
     app* zero;
     enode* e;
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index f85158e05..08ed144a3 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -299,7 +299,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) { init_zero(); return a.is_int(s) ? m_izero : m_rzero; }
+        th_var get_zero(sort* s) { return a.is_int(s) ? m_izero : m_rzero; }
 
         th_var get_zero(expr* e) { 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 5d2e23163..046a464c9 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -261,6 +261,7 @@ namespace smt {
     template<typename Ext>
     void theory_utvpi<Ext>::init(context* ctx) {
         theory::init(ctx);
+        init_zero();
     }
 
     template<typename Ext>