From 43eb8623742e90a1361cac5ab64c2b87b39466df Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 8 Jan 2021 12:50:36 -0800
Subject: [PATCH] fix #4932

---
 src/smt/smt_conflict_resolution.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index ba8086088..d581ed4e5 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -794,6 +794,11 @@ namespace smt {
         if (is_eq && is_quantifier(f2)) {
             f2 = m_ctx.get_enode(f2)->get_owner();
         }
+        if (m.is_false(fact) && !m_ctx.is_true(n2) && !m_ctx.is_false(n2)) {          
+            pr = m.mk_hypothesis(m.mk_eq(n1_owner, n2_owner));
+            m_new_proofs.push_back(pr);
+            return pr;
+        }
         if (!is_eq || (f1 != n2_owner && f2 != n2_owner)) {
             CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2),
                    tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n";