mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix regression introduced in #6143
This commit is contained in:
parent
e1a00f4917
commit
c672c3a250
|
@ -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();
|
||||
|
|
Loading…
Reference in a new issue