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()););