From d3e4dd69f8c20f7a0ff1e81b03250732aa150604 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 3 May 2020 11:18:31 -0700
Subject: [PATCH] relax condition on theory disequality propagation fix #4194

---
 src/smt/smt_context_inv.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index fefb3a78a..92a08df14 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -276,6 +276,8 @@ namespace smt {
                     enode * rhs = n->get_arg(1)->get_root();
                     if (rhs->is_interpreted() && lhs->is_interpreted())
                         continue;
+                    if (lhs == rhs)
+                        continue;
                     TRACE("check_th_diseq_propagation", tout << "num. theory_vars: " << lhs->get_num_th_vars() << " " 
                           << mk_pp(m.get_sort(lhs->get_owner()), m) << "\n";);
                     theory_var_list * l = lhs->get_th_var_list();