From c672c3a250adf0512784d4a7d3504bbd8c70c696 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 25 Oct 2022 09:39:11 -0700
Subject: [PATCH] fix regression introduced in #6143

---
 src/sat/sat_simplifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 97405fb32..b456db243 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -2000,7 +2000,7 @@ namespace sat {
         m_elim_counter -= num_pos * num_neg + before_lits;
 
         for (auto & c1 : m_pos_cls) {
-            if (c1.was_removed())
+            if (c1.was_removed() && !c1.contains(pos_l))
                 continue;
             for (auto & c2 : m_neg_cls) {
                 m_new_cls.reset();