From 767dff4a5ac8219095dd48d1eebbfe77d348a356 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 16 Apr 2020 17:55:23 -0700 Subject: [PATCH] fix #3903 Signed-off-by: Nikolaj Bjorner --- src/smt/diff_logic.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 293d091df..9e7afcb90 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -409,10 +409,13 @@ private: if (gamma < m_gamma[target]) { m_gamma[target] = gamma; m_parent[target] = e_id; + SASSERT(m_heap.contains(target)); m_heap.decreased(target); } break; case DL_PROCESSED: + // if two edges with the same source/target occur in the graph. + break; default: UNREACHABLE(); } @@ -425,7 +428,6 @@ private: m_assignment_stack.reset(); return true; } - source = m_heap.erase_min(); m_mark[source] = DL_PROCESSED; acc_assignment(source, m_gamma[source]);