diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index e5a7d4ff0f2..bf2f6ae1cee 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -5617,7 +5617,17 @@ void smt2_convt::find_symbols(const exprt &expr)
       convert_type(array_type);
       out << ")" << "\n";
 
-      if(!is_zero_width(array_type.element_type(), ns))
+      // Per-element constraints enumerate indices via from_integer(i,
+      // index_type); this is only possible for integer/bitvector index types.
+      // For arrays keyed by a non-scalar type (e.g. Strata's `Map Ref _`), we
+      // leave the array unconstrained (sound over-approximation).
+      const typet &idx_t = array_type.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 ||
+        idx_t.id() == ID_c_bool;
+      if(!is_zero_width(array_type.element_type(), ns) && int_index)
       {
         for(std::size_t i = 0; i < expr.operands().size(); i++)
         {