Mark fixed_eq literals as relevant (#7533)

Z3Prover · Jan 27, 2025 · 2d8f024 · 2d8f024
1 parent 63f9fda
commit 2d8f024
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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) << " "