From 9531c5e1679d2a19f2bef3bec21fe58e02b72bd0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Apr 2020 10:45:57 -0700 Subject: [PATCH] fix #3573 fix #3723 Signed-off-by: Nikolaj Bjorner --- src/smt/diff_logic.h | 3 ++- src/smt/theory_utvpi_def.h | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) 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); );