From 2d8f02468025d384ed854b5799222a9d3a17c26f Mon Sep 17 00:00:00 2001
From: Can Cebeci <can.cebeci99@gmail.com>
Date: Mon, 27 Jan 2025 20:10:46 +0100
Subject: [PATCH] Mark fixed_eq literals as relevant (#7533)

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

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) << " "