diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 8310de561..26091dbc5 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -441,6 +441,8 @@ namespace smt {
         app* o1 = get_enode(v1)->get_expr();
         app* o2 = get_enode(v2)->get_expr();
         literal oeq = mk_eq(o1, o2, true);
+        ctx.mark_as_relevant(oeq);
+
         unsigned sz = get_bv_size(v1);
         TRACE("bv", 
               tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << " "