diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index e5a7d4ff0f2..d76c4fb3128 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -1923,15 +1923,30 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     auto element_size_expr_opt =
       ::size_of_expr(element_address_expr.element_type(), ns);
-    CHECK_RETURN(element_size_expr_opt.has_value());
-
-    out << "(element-address-" << type2id(expr.type()) << ' ';
+    // The size/offset arithmetic requires an integer index type. Heap arrays
+    // keyed by a non-integer type (Strata `Map Ref _`) or with mathematical
+    // element types have neither a sensible byte size nor an integer index;
+    // fall back to an integer index type and unit size to avoid building a
+    // constant of a struct type.
+    const typet &idx_t = element_address_expr.index().type();
+    const bool int_index =
+      idx_t.id() == ID_unsignedbv || idx_t.id() == ID_signedbv ||
+      idx_t.id() == ID_bv || idx_t.id() == ID_integer ||
+      idx_t.id() == ID_c_enum || idx_t.id() == ID_c_enum_tag;
+    const typet size_target = int_index ? idx_t : c_index_type();
+    const exprt element_size_expr =
+      element_size_expr_opt.has_value()
+        ? *element_size_expr_opt
+        : static_cast<exprt>(from_integer(1, size_target));
+
+    out << "(element-address-" << type2id(expr.type()) << '_' << type2id(idx_t)
+        << ' ';
     convert_expr(element_address_expr.base());
     out << ' ';
     convert_expr(element_address_expr.index());
     out << ' ';
-    convert_expr(typecast_exprt::conditional_cast(
-      *element_size_expr_opt, element_address_expr.index().type()));
+    convert_expr(
+      typecast_exprt::conditional_cast(element_size_expr, size_target));
     out << ')';
   }
   else if(expr.id() == ID_field_address)
@@ -5974,7 +5989,8 @@ void smt2_convt::find_symbols(const exprt &expr)
   }
   else if(expr.id() == ID_element_address)
   {
-    irep_idt function = "element-address-" + type2id(expr.type());
+    irep_idt function = "element-address-" + type2id(expr.type()) + "_" +
+                        type2id(to_element_address_expr(expr).index().type());
 
     if(state_fkt_declared.insert(function).second)
     {
@@ -5983,7 +5999,17 @@ void smt2_convt::find_symbols(const exprt &expr)
       out << ' ';
       convert_type(to_element_address_expr(expr).index().type());
       out << ' '; // repeat, for the element size
-      convert_type(to_element_address_expr(expr).index().type());
+      // The size argument is built as an integer (see convert_expr for
+      // ID_element_address); for non-integer (e.g. struct-keyed) index types
+      // we fall back to c_index_type rather than the index type itself.
+      {
+        const typet &idx_t = to_element_address_expr(expr).index().type();
+        const bool int_index =
+          idx_t.id() == ID_unsignedbv || idx_t.id() == ID_signedbv ||
+          idx_t.id() == ID_bv || idx_t.id() == ID_integer ||
+          idx_t.id() == ID_c_enum || idx_t.id() == ID_c_enum_tag;
+        convert_type(int_index ? idx_t : c_index_type());
+      }
       out << ") ";
       convert_type(expr.type()); // return type
       out << ")\n";              // declare-fun