relax condition on theory disequality propagation fix #4194

Z3Prover · May 3, 2020 · d3e4dd6 · d3e4dd6
1 parent fcab7e4
commit d3e4dd6
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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();