From dc31478d8246987bb741b21fc1591ea6a2c5cf8e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 26 Feb 2020 20:53:51 -0800
Subject: [PATCH] detect conflicts in cut_simplifier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_cut_simplifier.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

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);