diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 8496717eb..8fb6ff95d 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -434,6 +434,7 @@ namespace bv {
         SASSERT(bv.is_int2bv(n));
         euf::enode* e = expr2enode(n);
         mk_bits(e->get_th_var(get_id()));
+        get_var(e->get_arg(0));
         assert_int2bv_axiom(n);
     }
 
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index bc435d7eb..5ed7c1a27 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -208,7 +208,33 @@ namespace bv {
         if (is_bv(eq.v1())) {
             m_find.merge(eq.v1(), eq.v2());
             VERIFY(eq.is_eq());
+            return;
         }
+        euf::enode* n1 = var2enode(eq.v1());
+        euf::enode* int2bv = nullptr;
+        for (euf::enode* sib : euf::enode_class(n1)) {
+            if (bv.is_bv2int(sib->get_expr())) {
+                int2bv = sib;
+                break;
+            }
+        }
+        if (!int2bv)
+            return;
+
+        for (euf::enode* p : euf::enode_parents(n1->get_root())) {
+            if (bv.is_int2bv(p->get_expr())) {
+                euf::enode* int2bv_arg = int2bv->get_arg(0);
+                if (p->get_root() != int2bv_arg->get_root()) {
+                    euf::enode_pair_vector eqs;
+                    eqs.push_back({ n1, p->get_arg(0) });
+                    eqs.push_back({ n1, int2bv });
+                    ctx.propagate(p, int2bv_arg, euf::th_explain::propagate(*this, eqs, p, int2bv_arg));
+                    break;
+                }
+            }
+        }
+
+
     }
 
     void solver::new_diseq_eh(euf::th_eq const& ne) {
diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
index 6167d3b9b..7f4ff2f4d 100644
--- a/src/sat/smt/sat_th.cpp
+++ b/src/sat/smt/sat_th.cpp
@@ -270,6 +270,10 @@ namespace euf {
         return mk(th, lits.size(), lits.data(), eqs.size(), eqs.data(), sat::null_literal, x, y, pma);
     }
 
+    th_explain* th_explain::propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma) {
+        return mk(th, 0, nullptr, eqs.size(), eqs.data(), sat::null_literal, x, y, pma);
+    }
+
     th_explain* th_explain::propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y) {
         return mk(th, 1, &lit, 0, nullptr, sat::null_literal, x, y);
     }
diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h
index f699c864b..4484a7717 100644
--- a/src/sat/smt/sat_th.h
+++ b/src/sat/smt/sat_th.h
@@ -241,6 +241,7 @@ namespace euf {
         static th_explain* conflict(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
         static th_explain* conflict(th_euf_solver& th, euf::enode* x, euf::enode* y);
         static th_explain* propagate(th_euf_solver& th, sat::literal lit, euf::enode* x, euf::enode* y);
+        static th_explain* propagate(th_euf_solver& th, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma = nullptr);
         static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, sat::literal consequent, sat::proof_hint const* pma = nullptr);
         static th_explain* propagate(th_euf_solver& th, sat::literal_vector const& lits, enode_pair_vector const& eqs, euf::enode* x, euf::enode* y, sat::proof_hint const* pma = nullptr);