diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index b4290a198..a01fdd483 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1502,11 +1502,11 @@ namespace smt {
             // int2bv(bv2int(x)) = x when int2bv(bv2int(x)) has same sort as x
             enode* n1 = get_enode(r1);
             auto propagate_bv2int = [&](enode* bv2int) {
-                enode* bv2int_arg = bv2int->get_arg(0);
+                enode* bv2int_arg = get_arg(bv2int, 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, get_arg(p, 0) });
                         eqs.push_back({n1, bv2int});
                         justification * js = ctx.mk_justification(
                             ext_theory_eq_propagation_justification(get_id(), ctx, 0, nullptr, eqs.size(), eqs.data(), p, bv2int_arg));