From efa74fe6c6e50c260904243e7f33367b73eb8a09 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Jul 2022 12:20:36 -0700 Subject: [PATCH] fix #6180 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_simplifier.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 409d03652..97405fb32 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1812,9 +1812,9 @@ namespace sat { CTRACE("resolve_bug", !c1.contains(l) || !c2.contains(~l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";); if (m_visited.size() <= 2*s.num_vars()) m_visited.resize(2*s.num_vars(), false); - if (c1.was_removed()) + if (c1.was_removed() && !c1.contains(l)) return false; - if (c2.was_removed()) + if (c2.was_removed() && !c2.contains(~l)) return false; SASSERT(c1.contains(l)); SASSERT(c2.contains(~l));