avoid useless false equality literals

Z3Prover · Oct 7, 2020 · 546e152 · 546e152
1 parent 1d8d587
commit 546e152
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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()););