From b120923dd5dec11618da1f48b9a2936c8f567422 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 30 May 2018 11:54:57 -0700 Subject: [PATCH] qe_lite: bug fix in der::der_sort_vars() The case of VAR 1 = (+ (:var 2) 10) VAR 2 = (+ 0 foo) was not properly handled whenever VAR2 has only one reference. In that case, VAR2 is not marked as done when VAR1 is processed, causing VAR2 to be duplicated in elimination order --- src/qe/qe_lite.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 2a14aa6f2..296cb2ad2 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -142,10 +142,10 @@ namespace eq { } else { SASSERT(fr.second == 1); - visiting.reset_mark(t); + visiting.reset_mark(t); if (!done.is_marked(t)) { if (definitions.get(vidx, nullptr) != nullptr) - order.push_back(vidx); + order.push_back(vidx); done.mark(t); } } @@ -444,7 +444,7 @@ namespace eq { expr_ref r(m); m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr(), r); unsigned inx = sz - m_order[i]- 1; - SASSERT(m_subst_map[inx]==0); + SASSERT(m_subst_map[inx]==nullptr); m_subst_map[inx] = r; } }