From 17663acf75e294d9693cf7f9baa1b9d159d66494 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 25 Aug 2021 05:59:27 -0700
Subject: [PATCH] #5482 other relevancy tracking

---
 src/sat/smt/bv_internalize.cpp | 27 ++++++++++++++-------------
 1 file changed, 14 insertions(+), 13 deletions(-)

diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 4e5d0ab14..8c16d6052 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -423,9 +423,9 @@ namespace bv {
         for (expr* b : k_bits) 
             args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero));        
         expr_ref sum(m_autil.mk_add(sz, args.data()), m);
-        expr_ref eq = mk_eq(n, sum);
-        sat::literal lit = ctx.internalize(eq, false, false, m_is_redundant);
-        add_unit(lit);
+        sat::literal lit = eq_internalize(n, sum);
+	add_unit(lit);
+	ctx.add_root(lit);
     }
 
     void solver::internalize_int2bv(app* n) {
@@ -453,9 +453,9 @@ namespace bv {
         unsigned sz = bv.get_bv_size(n);
         numeral mod = power(numeral(2), sz);
         rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
-        expr_ref eq = mk_eq(lhs, rhs);
-        TRACE("bv", tout << eq << "\n";);
-        add_unit(ctx.internalize(eq, false, false, m_is_redundant));
+	sat::literal eq_lit = eq_internalize(lhs, rhs);
+	add_unit(eq_lit);
+	ctx.add_root(eq_lit);
        
         expr_ref_vector n_bits(m);
         get_bits(n_enode, n_bits);
@@ -466,9 +466,9 @@ namespace bv {
             rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2));
             rhs = mk_eq(rhs, m_autil.mk_int(1));
             lhs = n_bits.get(i);
-            expr_ref eq = mk_eq(lhs, rhs);
-            TRACE("bv", tout << eq << "\n";);
-            add_unit(ctx.internalize(eq, false, false, m_is_redundant));
+	    eq_lit = eq_internalize(lhs, rhs);
+	    add_unit(eq_lit);
+	    ctx.add_root(eq_lit);
         }
     }
 
@@ -650,7 +650,9 @@ namespace bv {
             conc.push_back(arg);
         expr_ref r(bv.mk_concat(conc), m);
         mk_bits(get_th_var(e));
-        add_unit(eq_internalize(e, r));
+	sat::literal eq_lit = eq_internalize(e, r);
+        add_unit(eq_lit);
+	ctx.add_root(eq_lit);
     }
 
     void solver::internalize_bit2bool(app* n) {
@@ -760,9 +762,8 @@ namespace bv {
             expr_ref e1(m), e2(m);
             e1 = bv.mk_bit2bool(o1, i);
             e2 = bv.mk_bit2bool(o2, i);
-            expr_ref e = mk_eq(e1, e2);
-            literal eq = ctx.internalize(e, false, false, m_is_redundant);
-            add_clause(eq, ~oeq);
+            literal eq = eq_internalize(e1, e2);
+	    add_clause(eq, ~oeq);
             eqs.push_back(~eq);
         }
         TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);