From 546e15283781ed710dc297404bbc5ecb058cd0b8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Oct 2020 18:01:01 -0700
Subject: [PATCH] avoid useless false equality literals

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

diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
index de70fcdaf..99d494b72 100644
--- a/src/smt/smt_theory.cpp
+++ b/src/smt/smt_theory.cpp
@@ -132,6 +132,8 @@ namespace smt {
         if (a == b) {
             return true_literal;
         }
+        if (m.are_distinct(a, b))
+            return false_literal;
         app_ref eq(ctx.mk_eq_atom(a, b), get_manager());
         TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n";
               tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager()););