diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index e5a7d4ff0f2..fdd3d164d3c 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -4552,10 +4552,23 @@ void smt2_convt::convert_with(const with_exprt &expr)
 
     if(use_array_theory(expr))
     {
+      const typet idx_type = array_type.index_type();
+      const auto is_bv = [](const typet &t)
+      {
+        return t.id() == ID_unsignedbv || t.id() == ID_signedbv ||
+               t.id() == ID_c_bool || t.id() == ID_c_enum ||
+               t.id() == ID_c_enum_tag;
+      };
+      const exprt where =
+        (idx_type != expr.where().type() && is_bv(idx_type) &&
+         is_bv(expr.where().type()))
+          ? static_cast<exprt>(typecast_exprt(expr.where(), idx_type))
+          : expr.where();
+
       out << "(store ";
       convert_expr(expr.old());
       out << " ";
-      convert_expr(typecast_exprt(expr.where(), array_type.index_type()));
+      convert_expr(where);
       out << " ";
       convert_expr(expr.new_value());
       out << ")";
@@ -4768,13 +4781,29 @@ void smt2_convt::convert_index(const index_exprt &expr)
 
     if(use_array_theory(expr.array()))
     {
+      // Typecast the index to the array's index type, but only when both
+      // types are fixed-width bitvectors. For mathematical integers or
+      // struct-typed indices (e.g., map keys), emit directly.
+      const typet idx_type = array_type.index_type();
+      const auto is_bv = [](const typet &t)
+      {
+        return t.id() == ID_unsignedbv || t.id() == ID_signedbv ||
+               t.id() == ID_c_bool || t.id() == ID_c_enum ||
+               t.id() == ID_c_enum_tag;
+      };
+      const exprt index =
+        (idx_type != expr.index().type() && is_bv(idx_type) &&
+         is_bv(expr.index().type()))
+          ? static_cast<exprt>(typecast_exprt(expr.index(), idx_type))
+          : expr.index();
+
       if(expr.is_boolean() && !use_array_of_bool)
       {
         out << "(= ";
         out << "(select ";
         convert_expr(expr.array());
         out << " ";
-        convert_expr(typecast_exprt(expr.index(), array_type.index_type()));
+        convert_expr(index);
         out << ")";
         out << " #b1)";
       }
@@ -4783,7 +4812,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
         out << "(select ";
         convert_expr(expr.array());
         out << " ";
-        convert_expr(typecast_exprt(expr.index(), array_type.index_type()));
+        convert_expr(index);
         out << ")";
       }
     }