diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 5ed7c1a27..2a39fae6a 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -211,30 +211,20 @@ namespace bv {
             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()) {
+        for (euf::enode* bv2int : euf::enode_class(n1)) {
+            if (!bv.is_bv2int(bv2int->get_expr()))
+                continue;
+            euf::enode* bv2int_arg = bv2int->get_arg(0);
+            for (euf::enode* p : euf::enode_parents(n1->get_root())) {
+                if (bv.is_int2bv(p->get_expr()) && p->get_sort() == bv2int_arg->get_sort() && p->get_root() != bv2int_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));
+                    eqs.push_back({ n1, bv2int });
+                    ctx.propagate(p, bv2int_arg, euf::th_explain::propagate(*this, eqs, p, bv2int_arg));
                     break;
                 }
             }
         }
-
-
     }
 
     void solver::new_diseq_eh(euf::th_eq const& ne) {
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 2a70e884d..dba402a6e 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1497,32 +1497,24 @@ namespace smt {
         bool changed = true;
         TRACE("bv", tout << "bits size: " << sz << "\n";);
         if (sz == 0) {
+            // int2bv(bv2int(x)) = x when int2bv(bv2int(x)) has same sort as x
             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()) {                        
+            for (enode* bv2int : *n1) {
+                if (!m_util.is_bv2int(bv2int->get_expr())) 
+                    continue;
+                enode* bv2int_arg = bv2int->get_arg(0);
+                for (enode* p : enode::parents(n1->get_root())) {
+                    if (m_util.is_int2bv(p->get_expr()) && p->get_root() != bv2int_arg->get_root() && p->get_sort() == bv2int_arg->get_sort()) {                        
                         enode_pair_vector eqs;
                         eqs.push_back({n1, p->get_arg(0) });
-                        eqs.push_back({n1, int2bv});
+                        eqs.push_back({n1, bv2int});
                         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));
+                            ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), 0, nullptr, eqs.size(), eqs.data(), p, bv2int_arg));
+                        ctx.assign_eq(p, bv2int_arg, eq_justification(js));
                         break;
                     }                    
                 }
             }
-
         }
         do {
             // This outerloop is necessary to avoid missing propagation steps.