From 0b063f7903f3f7b14fb42d59d8d15239fa67a69d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Aug 2021 12:50:24 -0700
Subject: [PATCH] #5518

---
 src/ast/euf/euf_egraph.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 79426202b..fd93ce943 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -422,6 +422,11 @@ namespace euf {
             set_conflict(n1, n2, j);
             return;
         }
+        if (r1->value() != r2->value() && r1->value() != l_undef && r2->value() != l_undef) {
+            SASSERT(m.is_bool(r1->get_expr()));
+            set_conflict(n1, n2, j);
+            return;
+        }
         if (!r2->interpreted() && 
              (r1->class_size() > r2->class_size() || r1->interpreted() || r1->value() != l_undef)) {
             std::swap(r1, r2);