From d016cb1da5768317193237982fb5be2956a02851 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 16 Jun 2021 23:57:44 -0500
Subject: [PATCH] #5336

---
 src/ast/euf/euf_enode.h    | 1 +
 src/sat/smt/euf_solver.cpp | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/ast/euf/euf_enode.h b/src/ast/euf/euf_enode.h
index 218ffb3e5..d2b4cf02a 100644
--- a/src/ast/euf/euf_enode.h
+++ b/src/ast/euf/euf_enode.h
@@ -156,6 +156,7 @@ namespace euf {
         bool interpreted() const { return m_interpreted; }
         bool is_equality() const { return m_is_equality; }
         lbool value() const { return m_value;  }
+        bool value_conflict() const { return value() != l_undef && get_root()->value() != l_undef && value() != get_root()->value(); }
         sat::bool_var bool_var() const { return m_bool_var; }
         bool is_cgr() const { return this == m_cg; }
         enode* get_cg() const { return m_cg; }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 9d3cc9716..66b373b6f 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -294,7 +294,7 @@ namespace euf {
         euf::enode* n = m_egraph.find(e);
         if (!n)
             return;
-        bool sign = l.sign();                
+        bool sign = l.sign();       
         m_egraph.set_value(n, sign ? l_false : l_true);
         for (auto th : enode_th_vars(n))
             m_id2solver[th.get_id()]->asserted(l);
@@ -308,7 +308,7 @@ namespace euf {
             euf::enode* nb = n->get_arg(1);
             m_egraph.merge(na, nb, c);
         }
-        else if (n->merge_tf()) {
+        else if (n->merge_tf() || n->value_conflict()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
         }