diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp index 641a4b703..4091a9cc9 100644 --- a/src/sat/sat_cut_simplifier.cpp +++ b/src/sat/sat_cut_simplifier.cpp @@ -358,6 +358,13 @@ namespace sat { } while (first != idx); } + for (unsigned i = s.num_vars(); i-- > 0; ) { + literal lit(i, false); + if (uf2.find(lit.index()) == uf2.find((~lit).index())) { + s.set_conflict(); + return; + } + } if (new_eq) { elim_eqs elim(s); elim(uf2);