diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index 4958a14de..c66147756 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -1268,7 +1268,8 @@ public:
         m_dfs_time[v] = 0;
         succ.push_back(v);
         numeral gamma;
-        for (dl_var w : succ) {
+        for (unsigned i = 0; i < succ.size(); ++i) { // succ is updated inside of lopp
+            dl_var w = succ[i];
             for (edge_id e_id : m_out_edges[w]) {
                 edge & e = m_edges[e_id];
                 if (e.is_enabled() && set_gamma(e, gamma).is_zero()) {
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 1d72d5e1c..1009fee43 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -757,7 +757,7 @@ namespace smt {
             }
 
             TRACE("utvpi", 
-                  tout << "Disparity: " << v1 << "\n";
+                  tout << "Disparity: " << v1 << " - " << v2 << "\n";
                   tout << "decrement: " << zero_v << "\n";
                   display(tout);
                   );