From de41cfd2772193016566b0c4dfc2b8d4cf71852f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Jul 2022 12:23:24 -0700
Subject: [PATCH] fix #6104

add equality reasoning to bit-vector solver to instantiate int2bv(bv2int(x)) = x identity on demand.
---
 src/smt/theory_bv.cpp | 39 +++++++++++++++++++++++++++++++++------
 1 file changed, 33 insertions(+), 6 deletions(-)

diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 90c8cd89e..2a70e884d 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -52,9 +52,8 @@ namespace smt {
         bits.reset();
         m_bits_expr.reset();
 
-        for (unsigned i = 0; i < bv_size; i++) {
+        for (unsigned i = 0; i < bv_size; i++) 
             m_bits_expr.push_back(mk_bit2bool(owner, i));
-        }
         ctx.internalize(m_bits_expr.data(), bv_size, true);
 
         for (unsigned i = 0; i < bv_size; i++) {
@@ -601,9 +600,8 @@ namespace smt {
         TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";);
         process_args(n);
         mk_enode(n);
-        if (!ctx.relevancy()) {
+        if (!ctx.relevancy()) 
             assert_bv2int_axiom(n);
-        }
     }
 
 
@@ -669,10 +667,11 @@ namespace smt {
         mk_enode(n);
         theory_var v = ctx.get_enode(n)->get_th_var(get_id()); 
         mk_bits(v);
+        mk_var(ctx.get_enode(n->get_arg(0)));
 
-        if (!ctx.relevancy()) {
+        
+        if (!ctx.relevancy()) 
             assert_int2bv_axiom(n);
-        }
     }
     
     void theory_bv::assert_int2bv_axiom(app* n) {
@@ -1497,6 +1496,34 @@ namespace smt {
         unsigned sz  = m_bits[v1].size();
         bool changed = true;
         TRACE("bv", tout << "bits size: " << sz << "\n";);
+        if (sz == 0) {
+            enode* n1 = get_enode(r1);
+            enode* int2bv = nullptr;
+            for (enode* sib : *n1) {
+                if (m_util.is_bv2int(sib->get_expr())) {
+                    int2bv = sib;
+                    break;
+                }
+            }
+            if (!int2bv)
+                return;
+            
+            for (enode* p : enode::parents(n1->get_root())) {
+                if (m_util.is_int2bv(p->get_expr())) {
+                    enode* int2bv_arg = int2bv->get_arg(0);
+                    if (p->get_root() != int2bv_arg->get_root()) {                        
+                        enode_pair_vector eqs;
+                        eqs.push_back({n1, p->get_arg(0) });
+                        eqs.push_back({n1, int2bv});
+                        justification * js = ctx.mk_justification(
+                            ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), 0, nullptr, eqs.size(), eqs.data(), p, int2bv_arg));
+                        ctx.assign_eq(p, int2bv_arg, eq_justification(js));
+                        break;
+                    }                    
+                }
+            }
+
+        }
         do {
             // This outerloop is necessary to avoid missing propagation steps.
             // For example, let's assume that bits1 and bits2 contains the following