diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index cf727b3f57d..d481eac8eb5 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -262,7 +262,7 @@ void rw_range_sett::get_objects_index(
   {
     const vector_typet &vector_type=to_vector_type(type);
 
-    auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
+    auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
 
     sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
   }
@@ -270,7 +270,7 @@ void rw_range_sett::get_objects_index(
   {
     const array_typet &array_type=to_array_type(type);
 
-    auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
+    auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
 
     sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
   }
@@ -301,7 +301,7 @@ void rw_range_sett::get_objects_array(
 {
   const array_typet &array_type = expr.type();
 
-  auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
+  auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
 
   range_spect sub_size;
 
@@ -608,7 +608,7 @@ void rw_range_sett::get_objects_rec(const typet &type)
   if(type.id()==ID_array)
   {
     const auto &array_type = to_array_type(type);
-    get_objects_rec(array_type.subtype());
+    get_objects_rec(array_type.element_type());
     get_objects_rec(get_modet::READ, array_type.size());
   }
 }
diff --git a/src/analyses/variable-sensitivity/abstract_aggregate_object.h b/src/analyses/variable-sensitivity/abstract_aggregate_object.h
index 43a6bca6368..36817ee3dc4 100644
--- a/src/analyses/variable-sensitivity/abstract_aggregate_object.h
+++ b/src/analyses/variable-sensitivity/abstract_aggregate_object.h
@@ -164,7 +164,7 @@ struct array_aggregate_typet
   static typet read_type(const typet &, const typet &object_type)
   {
     array_typet array_type(to_array_type(object_type));
-    return array_type.subtype();
+    return array_type.element_type();
   }
 
   static void get_statistics(
diff --git a/src/ansi-c/c_expr.cpp b/src/ansi-c/c_expr.cpp
index d89c05e9a8b..06108fcde5a 100644
--- a/src/ansi-c/c_expr.cpp
+++ b/src/ansi-c/c_expr.cpp
@@ -23,8 +23,8 @@ shuffle_vector_exprt::shuffle_vector_exprt(
     op1() = std::move(*vector2);
 
   const vector_typet &vt = to_vector_type(op0().type());
-  type() =
-    vector_typet{vt.subtype(), from_integer(indices.size(), vt.size().type())};
+  type() = vector_typet{vt.element_type(),
+                        from_integer(indices.size(), vt.size().type())};
 
   op2().operands().swap(indices);
 }
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index abe6ac6a9d8..194e9f6a0ab 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -223,8 +223,9 @@ bool check_c_implicit_typecast(
       }
     }
 
-    if(dest_type.id()==ID_array &&
-       src_type.subtype()==dest_type.subtype())
+    if(
+      dest_type.id() == ID_array &&
+      src_type.subtype() == to_array_type(dest_type).element_type())
       return false;
 
     if(dest_type.id()==ID_bool ||
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 90f49e4faff..d15883cda70 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -3388,15 +3388,16 @@ bool c_typecheck_baset::gcc_vector_types_compatible(
     return false;
 
   // compare subtype
-  if((type0.subtype().id()==ID_signedbv ||
-      type0.subtype().id()==ID_unsignedbv) &&
-     (type1.subtype().id()==ID_signedbv ||
-      type1.subtype().id()==ID_unsignedbv) &&
-     to_bitvector_type(type0.subtype()).get_width()==
-     to_bitvector_type(type1.subtype()).get_width())
+  if(
+    (type0.element_type().id() == ID_signedbv ||
+     type0.element_type().id() == ID_unsignedbv) &&
+    (type1.element_type().id() == ID_signedbv ||
+     type1.element_type().id() == ID_unsignedbv) &&
+    to_bitvector_type(type0.element_type()).get_width() ==
+      to_bitvector_type(type1.element_type()).get_width())
     return true;
 
-  return type0.subtype()==type1.subtype();
+  return type0.element_type() == type1.element_type();
 }
 
 void c_typecheck_baset::typecheck_expr_binary_arithmetic(exprt &expr)
diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
index f5162f5b6af..9e9ad06dccb 100644
--- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
+++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
@@ -1440,7 +1440,8 @@ exprt c_typecheck_baset::typecheck_shuffle_vector(
     CHECK_RETURN(input_size.has_value());
     if(arg1.has_value())
       input_size = *input_size * 2;
-    constant_exprt size = from_integer(*input_size, indices_type.subtype());
+    constant_exprt size =
+      from_integer(*input_size, indices_type.element_type());
 
     for(std::size_t i = 0; i < indices_size; ++i)
     {
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 8bf35e658cb..ce7ebcc67b3 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -318,7 +318,7 @@ void c_typecheck_baset::designator_enter(
     if(array_type.size().is_nil())
     {
       entry.size=0;
-      entry.subtype=array_type.subtype();
+      entry.subtype = array_type.element_type();
     }
     else
     {
@@ -332,7 +332,7 @@ void c_typecheck_baset::designator_enter(
       }
 
       entry.size = numeric_cast_v<std::size_t>(*array_size);
-      entry.subtype=array_type.subtype();
+      entry.subtype = array_type.element_type();
     }
   }
   else if(full_type.id()==ID_vector)
@@ -350,7 +350,7 @@ void c_typecheck_baset::designator_enter(
     }
 
     entry.size = numeric_cast_v<std::size_t>(*vector_size);
-    entry.subtype=vector_type.subtype();
+    entry.subtype = vector_type.element_type();
   }
   else
     UNREACHABLE;
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 2c61f525b0d..7dd5870cc7a 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -526,10 +526,10 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
   const source_locationt size_source_location = size.find_source_location();
 
   // check subtype
-  typecheck_type(type.subtype());
+  typecheck_type(type.element_type());
 
   // we don't allow void as subtype
-  if(type.subtype().id() == ID_empty)
+  if(type.element_type().id() == ID_empty)
   {
     error().source_location=type.source_location();
     error() << "array of voids" << eom;
@@ -537,7 +537,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
   }
 
   // we don't allow incomplete structs or unions as subtype
-  const typet &followed_subtype = follow(type.subtype());
+  const typet &followed_subtype = follow(type.element_type());
 
   if(
     (followed_subtype.id() == ID_struct || followed_subtype.id() == ID_union) &&
@@ -550,7 +550,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
   }
 
   // we don't allow functions as subtype
-  if(type.subtype().id() == ID_code)
+  if(type.element_type().id() == ID_code)
   {
     // ISO/IEC 9899 6.7.5.2
     error().source_location = type.source_location();
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index b4aff20aa69..0ef23976297 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -586,7 +586,7 @@ std::string expr2ct::convert_rec(
     const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());
     std::string dest="__gcc_v"+integer2string(size_int);
 
-    std::string tmp=convert(vector_type.subtype());
+    std::string tmp = convert(vector_type.element_type());
 
     if(tmp=="signed char" || tmp=="char")
       dest+="qi";
@@ -602,7 +602,7 @@ std::string expr2ct::convert_rec(
       dest+="df";
     else
     {
-      const std::string subtype=convert(vector_type.subtype());
+      const std::string subtype = convert(vector_type.element_type());
       dest=subtype;
       dest+=" __attribute__((vector_size (";
       dest+=convert(vector_type.size());
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 1b3d60882e5..4065997d636 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -313,10 +313,11 @@ void cpp_declarator_convertert::combine_types(
   }
   else if(symbol.type==decl_type)
     return; // ok
-  else if(symbol.type.id()==ID_array &&
-          symbol.type.find(ID_size).is_nil() &&
-          decl_type.id()==ID_array &&
-          symbol.type.subtype()==decl_type.subtype())
+  else if(
+    symbol.type.id() == ID_array &&
+    to_array_type(symbol.type).size().is_nil() && decl_type.id() == ID_array &&
+    to_array_type(symbol.type).element_type() ==
+      to_array_type(decl_type).element_type())
   {
     symbol.type = decl_type;
     return; // ok
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index e7c40d9d4b4..bcdc6b8a0bc 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -794,7 +794,7 @@ void cpp_typecheckt::check_fixed_size_array(typet &type)
     }
 
     // recursive call for multi-dimensional arrays
-    check_fixed_size_array(array_type.subtype());
+    check_fixed_size_array(array_type.element_type());
   }
 }
 
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index 11b28bdbee1..ab3029440a3 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -244,8 +244,8 @@ void cpp_typecheckt::zero_initializer(
     for(mp_integer i=0; i<size; ++i)
     {
       index_exprt index(
-        object, from_integer(i, c_index_type()), array_type.subtype());
-      zero_initializer(index, array_type.subtype(), source_location, ops);
+        object, from_integer(i, c_index_type()), array_type.element_type());
+      zero_initializer(index, array_type.element_type(), source_location, ops);
     }
   }
   else if(final_type.id()==ID_union)
diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp
index c3991828d2c..60fa77887d7 100644
--- a/src/cpp/template_map.cpp
+++ b/src/cpp/template_map.cpp
@@ -23,8 +23,8 @@ void template_mapt::apply(typet &type) const
 {
   if(type.id()==ID_array)
   {
-    apply(type.subtype());
-    apply(static_cast<exprt &>(type.add(ID_size)));
+    apply(to_array_type(type).element_type());
+    apply(to_array_type(type).size());
   }
   else if(type.id()==ID_pointer)
   {
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 8eca747682a..6ffd6b73216 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -109,7 +109,7 @@ std::string graphml_witnesst::convert_assign_rec(
     forall_operands(it, assign.rhs())
     {
       index_exprt index(
-        assign.lhs(), from_integer(i++, c_index_type()), type.subtype());
+        assign.lhs(), from_integer(i++, c_index_type()), type.element_type());
       if(!result.empty())
         result+=' ';
       result+=convert_assign_rec(identifier, code_assignt(index, *it));
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index a4e73e46195..18bb23e48f3 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -487,7 +487,7 @@ exprt interpretert::get_value(
   {
     // Get size of array
     array_exprt result({}, to_array_type(real_type));
-    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    const exprt &size_expr = to_array_type(type).size();
     mp_integer subtype_size=get_size(type.subtype());
     mp_integer count;
     if(size_expr.id()!=ID_constant)
@@ -553,7 +553,7 @@ exprt interpretert::get_value(
   else if(real_type.id()==ID_array)
   {
     array_exprt result({}, to_array_type(real_type));
-    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    const exprt &size_expr = to_array_type(real_type).size();
 
     // Get size of array
     mp_integer subtype_size=get_size(type.subtype());
@@ -888,7 +888,7 @@ typet interpretert::concretize_type(const typet &type)
 {
   if(type.id()==ID_array)
   {
-    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    const exprt &size_expr = to_array_type(type).size();
     mp_vectort computed_size = evaluate(size_expr);
     if(computed_size.size()==1 &&
        computed_size[0]>=0)
@@ -1006,7 +1006,7 @@ mp_integer interpretert::get_size(const typet &type)
   }
   else if(type.id()==ID_array)
   {
-    const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
+    const exprt &size_expr = to_array_type(type).size();
 
     mp_integer subtype_size=get_size(type.subtype());
 
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 51970abe141..7c292be6810 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -136,7 +136,7 @@ bool interpretert::count_type_leaves(const typet &ty, mp_integer &result)
     if(array_size_vec.size()!=1)
       return true;
     mp_integer subtype_count;
-    if(count_type_leaves(at.subtype(), subtype_count))
+    if(count_type_leaves(at.element_type(), subtype_count))
       return true;
     result=array_size_vec[0]*subtype_count;
     return false;
@@ -205,12 +205,12 @@ bool interpretert::byte_offset_to_memory_offset(
       return true;
 
     mp_integer array_size=array_size_vec[0];
-    auto elem_size_bytes = pointer_offset_size(at.subtype(), ns);
+    auto elem_size_bytes = pointer_offset_size(at.element_type(), ns);
     if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
       return true;
 
     mp_integer elem_size_leaves;
-    if(count_type_leaves(at.subtype(), elem_size_leaves))
+    if(count_type_leaves(at.element_type(), elem_size_leaves))
       return true;
 
     mp_integer this_idx = offset / (*elem_size_bytes);
@@ -219,7 +219,7 @@ bool interpretert::byte_offset_to_memory_offset(
 
     mp_integer subtype_result;
     bool ret = byte_offset_to_memory_offset(
-      at.subtype(), offset % (*elem_size_bytes), subtype_result);
+      at.element_type(), offset % (*elem_size_bytes), subtype_result);
 
     result=subtype_result+(elem_size_leaves*this_idx);
     return ret;
@@ -280,12 +280,12 @@ bool interpretert::memory_offset_to_byte_offset(
     if(array_size_vec.size()!=1)
       return true;
 
-    auto elem_size = pointer_offset_size(at.subtype(), ns);
+    auto elem_size = pointer_offset_size(at.element_type(), ns);
     if(!elem_size.has_value())
       return true;
 
     mp_integer elem_count;
-    if(count_type_leaves(at.subtype(), elem_count))
+    if(count_type_leaves(at.element_type(), elem_count))
       return true;
 
     mp_integer this_idx=full_cell_offset/elem_count;
@@ -293,11 +293,8 @@ bool interpretert::memory_offset_to_byte_offset(
       return true;
 
     mp_integer subtype_result;
-    bool ret=
-      memory_offset_to_byte_offset(
-        at.subtype(),
-        full_cell_offset%elem_count,
-        subtype_result);
+    bool ret = memory_offset_to_byte_offset(
+      at.element_type(), full_cell_offset % elem_count, subtype_result);
     result = subtype_result + ((*elem_size) * this_idx);
     return ret;
   }
diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp
index 795e42972b4..7ce6a016048 100644
--- a/src/goto-programs/json_expr.cpp
+++ b/src/goto-programs/json_expr.cpp
@@ -153,13 +153,13 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
   else if(type.id() == ID_array)
   {
     result["name"] = json_stringt("array");
-    result["subtype"] = json(to_array_type(type).subtype(), ns, mode);
+    result["subtype"] = json(to_array_type(type).element_type(), ns, mode);
     result["size"] = json(to_array_type(type).size(), ns, mode);
   }
   else if(type.id() == ID_vector)
   {
     result["name"] = json_stringt("vector");
-    result["subtype"] = json(to_vector_type(type).subtype(), ns, mode);
+    result["subtype"] = json(to_vector_type(type).element_type(), ns, mode);
     result["size"] = json(to_vector_type(type).size(), ns, mode);
   }
   else if(type.id() == ID_struct)
diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp
index dc27e69be98..0da01d52f7f 100644
--- a/src/goto-programs/remove_vector.cpp
+++ b/src/goto-programs/remove_vector.cpp
@@ -116,7 +116,7 @@ static void remove_vector(exprt &expr)
       const mp_integer dimension =
         numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
-      const typet subtype=array_type.subtype();
+      const typet subtype = array_type.element_type();
       // do component-wise:
       // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
       array_exprt array_expr({}, array_type);
@@ -144,7 +144,7 @@ static void remove_vector(exprt &expr)
       const mp_integer dimension =
         numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
-      const typet subtype=array_type.subtype();
+      const typet subtype = array_type.element_type();
       // do component-wise:
       // -x -> vector(-x[0],-x[1],...)
       array_exprt array_expr({}, array_type);
@@ -173,7 +173,7 @@ static void remove_vector(exprt &expr)
       const vector_typet &vector_type = to_vector_type(expr.type());
       const auto dimension = numeric_cast_v<std::size_t>(vector_type.size());
 
-      const typet &subtype = vector_type.subtype();
+      const typet &subtype = vector_type.element_type();
       PRECONDITION(subtype.id() == ID_signedbv);
       exprt minus_one = from_integer(-1, subtype);
       exprt zero = from_integer(0, subtype);
@@ -237,7 +237,7 @@ static void remove_vector(exprt &expr)
         const auto dimension =
           numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
         exprt casted_op =
-          typecast_exprt::conditional_cast(op, array_type.subtype());
+          typecast_exprt::conditional_cast(op, array_type.element_type());
         source_locationt source_location = expr.source_location();
         expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);
         expr.add_source_location() = std::move(source_location);
@@ -285,10 +285,10 @@ static void remove_vector(typet &type)
   {
     vector_typet &vector_type=to_vector_type(type);
 
-    remove_vector(type.subtype());
+    remove_vector(vector_type.element_type());
 
     // Replace by an array with appropriate number of members.
-    array_typet array_type(vector_type.subtype(), vector_type.size());
+    array_typet array_type(vector_type.element_type(), vector_type.size());
     array_type.add_source_location()=type.source_location();
     type=array_type;
   }
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 07790127f2a..116f011bf53 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -881,7 +881,7 @@ bool string_abstractiont::build_if(const if_exprt &o_if,
 bool string_abstractiont::build_array(const array_exprt &object,
     exprt &dest, bool write)
 {
-  PRECONDITION(is_char_type(object.type().subtype()));
+  PRECONDITION(is_char_type(object.type().element_type()));
 
   // writing is invalid
   if(write)
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
index df33dde42af..8aaf919ca9d 100644
--- a/src/goto-programs/xml_expr.cpp
+++ b/src/goto-programs/xml_expr.cpp
@@ -76,7 +76,7 @@ xmlt xml(const typet &type, const namespacet &ns)
   {
     result.name = "array";
     result.new_element("subtype").new_element() =
-      xml(to_array_type(type).subtype(), ns);
+      xml(to_array_type(type).element_type(), ns);
     result.new_element("size").new_element() =
       xml(to_array_type(type).size(), ns);
   }
@@ -84,7 +84,7 @@ xmlt xml(const typet &type, const namespacet &ns)
   {
     result.name = "vector";
     result.new_element("subtype").new_element() =
-      xml(to_vector_type(type).subtype(), ns);
+      xml(to_vector_type(type).element_type(), ns);
     result.new_element("size").new_element() =
       xml(to_vector_type(type).size(), ns);
   }
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index ac235b129e8..6f2d7fe9da7 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -131,7 +131,7 @@ void goto_symext::symex_assign(
 static std::string get_alnum_string(const array_exprt &char_array)
 {
   const auto &ibv_type =
-    to_integer_bitvector_type(to_array_type(char_array.type()).subtype());
+    to_integer_bitvector_type(to_array_type(char_array.type()).element_type());
 
   const std::size_t n_bits = ibv_type.get_width();
   CHECK_RETURN(n_bits % 8 == 0);
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index c6913794efc..b80011ee2f0 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -573,7 +573,7 @@ void goto_symex_statet::rename_address(exprt &expr, const namespacet &ns)
 
       rename_address<level>(index_expr.array(), ns);
       PRECONDITION(index_expr.array().type().id() == ID_array);
-      expr.type() = to_array_type(index_expr.array().type()).subtype();
+      expr.type() = to_array_type(index_expr.array().type()).element_type();
 
       // the index is not an address
       index_expr.index() =
@@ -632,7 +632,7 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
   if(type.id() == ID_array)
   {
     const auto &array_type = to_array_type(type);
-    return requires_renaming(array_type.subtype(), ns) ||
+    return requires_renaming(array_type.element_type(), ns) ||
            !array_type.size().is_constant();
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
@@ -719,7 +719,7 @@ void goto_symex_statet::rename(
   if(type.id()==ID_array)
   {
     auto &array_type = to_array_type(type);
-    rename<level>(array_type.subtype(), irep_idt(), ns);
+    rename<level>(array_type.element_type(), irep_idt(), ns);
     array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp
index bd3c2801366..69fc8684d93 100644
--- a/src/goto-symex/renaming_level.cpp
+++ b/src/goto-symex/renaming_level.cpp
@@ -175,7 +175,8 @@ typet get_original_name(typet type)
   if(type.id() == ID_array)
   {
     auto &array_type = to_array_type(type);
-    array_type.subtype() = get_original_name(std::move(array_type.subtype()));
+    array_type.element_type() =
+      get_original_name(std::move(array_type.element_type()));
     array_type.size() = get_original_name(std::move(array_type.size()));
   }
   else if(type.id() == ID_struct || type.id() == ID_union)
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index a991cb372a3..230468a18ad 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -102,7 +102,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
       // type T[N-(B/sizeof(T))]
       const array_typet &prev_array_type = to_array_type(expr.type());
       const typet &array_size_type = prev_array_type.size().type();
-      const typet &subtype = prev_array_type.subtype();
+      const typet &subtype = prev_array_type.element_type();
 
       exprt new_offset =
         typecast_exprt::conditional_cast(ode.offset(), array_size_type);
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 3c3393ff2cd..3539348e6b1 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -197,8 +197,8 @@ void goto_symext::symex_other(
 
     const array_typet &array_type = to_array_type(array_expr.type());
 
-    if(array_type.subtype() != value.type())
-      value = typecast_exprt(value, array_type.subtype());
+    if(array_type.element_type() != value.type())
+      value = typecast_exprt(value, array_type.element_type());
 
     symex_assign(state, array_expr, array_of_exprt(value, array_type));
   }
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index be187bfdc43..b709a03314a 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -679,8 +679,8 @@ void arrayst::add_array_constraints_array_of(
 
   for(const auto &index : index_set)
   {
-    const typet &subtype = expr.type().subtype();
-    index_exprt index_expr(expr, index, subtype);
+    const typet &element_type = expr.type().element_type();
+    index_exprt index_expr(expr, index, element_type);
 
     DATA_INVARIANT(
       index_expr.type() == expr.what().type(),
@@ -703,8 +703,8 @@ void arrayst::add_array_constraints_array_constant(
 
   for(const auto &index : index_set)
   {
-    const typet &subtype = expr.type().subtype();
-    const index_exprt index_expr{expr, index, subtype};
+    const typet &element_type = expr.type().element_type();
+    const index_exprt index_expr{expr, index, element_type};
 
     if(index.is_constant())
     {
diff --git a/src/solvers/flattening/boolbv_array_of.cpp b/src/solvers/flattening/boolbv_array_of.cpp
index 458430a3805..51a4ad3893c 100644
--- a/src/solvers/flattening/boolbv_array_of.cpp
+++ b/src/solvers/flattening/boolbv_array_of.cpp
@@ -29,7 +29,7 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   {
     // A zero-length array is acceptable;
     // an element with unknown size is not.
-    if(boolbv_width(array_type.subtype())==0)
+    if(boolbv_width(array_type.element_type()) == 0)
       return conversion_failed(expr);
     else
       return bvt();
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index b81a3206817..a399606ae50 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -288,7 +288,7 @@ bvt boolbvt::convert_index(
 {
   const array_typet &array_type = to_array_type(array.type());
 
-  std::size_t width=boolbv_width(array_type.subtype());
+  std::size_t width = boolbv_width(array_type.element_type());
 
   if(width==0)
     return conversion_failed(array);
@@ -330,7 +330,7 @@ bvt boolbvt::convert_index(
     CHECK_RETURN(o.offset().id() != ID_unknown);
 
     const auto subtype_bytes_opt =
-      pointer_offset_size(array_type.subtype(), ns);
+      pointer_offset_size(array_type.element_type(), ns);
     CHECK_RETURN(subtype_bytes_opt.has_value());
 
     exprt new_offset = simplify_expr(
@@ -339,7 +339,7 @@ bvt boolbvt::convert_index(
       ns);
 
     byte_extract_exprt be =
-      make_byte_extract(o.root_object(), new_offset, array_type.subtype());
+      make_byte_extract(o.root_object(), new_offset, array_type.element_type());
 
     return convert_bv(be);
   }
@@ -350,7 +350,7 @@ bvt boolbvt::convert_index(
     const byte_extract_exprt &byte_extract_expr = to_byte_extract_expr(array);
 
     const auto subtype_bytes_opt =
-      pointer_offset_size(array_type.subtype(), ns);
+      pointer_offset_size(array_type.element_type(), ns);
     CHECK_RETURN(subtype_bytes_opt.has_value());
 
     // add offset to index
@@ -363,7 +363,7 @@ bvt boolbvt::convert_index(
 
     byte_extract_exprt be = byte_extract_expr;
     be.offset() = new_offset;
-    be.type() = array_type.subtype();
+    be.type() = array_type.element_type();
 
     return convert_bv(be);
   }
diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp
index e8b0b40c57a..260b9f56f91 100644
--- a/src/solvers/flattening/boolbv_update.cpp
+++ b/src/solvers/flattening/boolbv_update.cpp
@@ -73,7 +73,7 @@ void boolbvt::convert_update_rec(
     bvt index_bv = convert_bv(to_index_designator(designator).index());
 
     const array_typet &array_type=to_array_type(type);
-    const typet &subtype = array_type.subtype();
+    const typet &subtype = array_type.element_type();
     const exprt &size_expr = array_type.size();
 
     std::size_t element_size=boolbv_width(subtype);
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 90b9eda01b2..5cb7ff7d08c 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -123,7 +123,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   else if(type_id==ID_array)
   {
     const array_typet &array_type=to_array_type(type);
-    std::size_t sub_width=operator()(array_type.subtype());
+    std::size_t sub_width = operator()(array_type.element_type());
 
     const auto array_size = numeric_cast<mp_integer>(array_type.size());
 
@@ -146,7 +146,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   else if(type_id==ID_vector)
   {
     const vector_typet &vector_type=to_vector_type(type);
-    std::size_t sub_width=operator()(vector_type.subtype());
+    std::size_t sub_width = operator()(vector_type.element_type());
 
     const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
 
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
index b8d7ea0b542..5b7017d767d 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/src/solvers/lowering/byte_operators.cpp
@@ -159,7 +159,7 @@ static array_exprt bv_to_array_expr(
   const namespacet &ns)
 {
   auto num_elements = numeric_cast<std::size_t>(array_type.size());
-  auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
+  auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
 
   const std::size_t total_bits =
     to_bitvector_type(bitvector_expr.type()).get_width();
@@ -189,14 +189,14 @@ static array_exprt bv_to_array_expr(
       operands.push_back(bv_to_expr(
         extractbits_exprt{
           bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
-        array_type.subtype(),
+        array_type.element_type(),
         endianness_map,
         ns));
     }
     else
     {
-      operands.push_back(
-        bv_to_expr(bitvector_expr, array_type.subtype(), endianness_map, ns));
+      operands.push_back(bv_to_expr(
+        bitvector_expr, array_type.element_type(), endianness_map, ns));
     }
   }
 
@@ -213,7 +213,7 @@ static vector_exprt bv_to_vector_expr(
 {
   const std::size_t num_elements =
     numeric_cast_v<std::size_t>(vector_type.size());
-  auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
+  auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
   DATA_INVARIANT(
     !subtype_bits.has_value() ||
       *subtype_bits * num_elements ==
@@ -234,14 +234,14 @@ static vector_exprt bv_to_vector_expr(
       operands.push_back(bv_to_expr(
         extractbits_exprt{
           bitvector_expr, bounds.ub, bounds.lb, std::move(type)},
-        vector_type.subtype(),
+        vector_type.element_type(),
         endianness_map,
         ns));
     }
     else
     {
-      operands.push_back(
-        bv_to_expr(bitvector_expr, vector_type.subtype(), endianness_map, ns));
+      operands.push_back(bv_to_expr(
+        bitvector_expr, vector_type.element_type(), endianness_map, ns));
     }
   }
 
@@ -803,7 +803,7 @@ static exprt unpack_rec(
   if(src.type().id()==ID_array)
   {
     const array_typet &array_type=to_array_type(src.type());
-    const typet &subtype=array_type.subtype();
+    const typet &subtype = array_type.element_type();
 
     auto element_bits = pointer_offset_bits(subtype, ns);
     CHECK_RETURN(element_bits.has_value());
@@ -824,7 +824,7 @@ static exprt unpack_rec(
   else if(src.type().id() == ID_vector)
   {
     const vector_typet &vector_type = to_vector_type(src.type());
-    const typet &subtype = vector_type.subtype();
+    const typet &subtype = vector_type.element_type();
 
     auto element_bits = pointer_offset_bits(subtype, ns);
     CHECK_RETURN(element_bits.has_value());
@@ -1232,9 +1232,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
 
   optionalt<typet> subtype;
   if(root.type().id() == ID_vector)
-    subtype = to_vector_type(root.type()).subtype();
+    subtype = to_vector_type(root.type()).element_type();
   else
-    subtype = to_array_type(root.type()).subtype();
+    subtype = to_array_type(root.type()).element_type();
 
   auto subtype_bits = pointer_offset_bits(*subtype, ns);
 
@@ -2055,9 +2055,9 @@ static exprt lower_byte_update(
   {
     optionalt<typet> subtype;
     if(src.type().id() == ID_vector)
-      subtype = to_vector_type(src.type()).subtype();
+      subtype = to_vector_type(src.type()).element_type();
     else
-      subtype = to_array_type(src.type()).subtype();
+      subtype = to_array_type(src.type()).element_type();
 
     auto element_width = pointer_offset_bits(*subtype, ns);
     CHECK_RETURN(element_width.has_value());
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 6288a2b1151..a9729f417fc 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -536,7 +536,7 @@ void smt2_convt::walk_array_tree(
     if(failure)
       return;
     long index = tempint.to_long();
-    exprt value = parse_rec(src.get_sub()[3], type.subtype());
+    exprt value = parse_rec(src.get_sub()[3], type.element_type());
     operands_map->emplace(index, value);
   }
   else if(src.get_sub().size() == 3 && src.get_sub()[0].id() == "let")
@@ -553,7 +553,7 @@ void smt2_convt::walk_array_tree(
           src.get_sub()[0].get_sub()[1].id()=="const")
   {
     // (as const type_info default_value)
-    exprt default_value = parse_rec(src.get_sub()[1], type.subtype());
+    exprt default_value = parse_rec(src.get_sub()[1], type.element_type());
     operands_map->emplace(-1, default_value);
   }
 }
@@ -3383,9 +3383,11 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
       summands.reserve(expr.operands().size());
       for(const auto &op : expr.operands())
         summands.push_back(index_exprt(
-          op, from_integer(size - i - 1, index_type), vector_type.subtype()));
+          op,
+          from_integer(size - i - 1, index_type),
+          vector_type.element_type()));
 
-      plus_exprt tmp(std::move(summands), vector_type.subtype());
+      plus_exprt tmp(std::move(summands), vector_type.element_type());
 
       out << " ";
       convert_expr(tmp);
@@ -3575,13 +3577,12 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
     // subtract component-by-component
     for(mp_integer i=0; i!=size; ++i)
     {
-      exprt tmp(ID_minus, vector_type.subtype());
+      exprt tmp(ID_minus, vector_type.element_type());
       forall_operands(it, expr)
-        tmp.copy_to_operands(
-          index_exprt(
-            *it,
-            from_integer(size-i-1, index_type),
-            vector_type.subtype()));
+        tmp.copy_to_operands(index_exprt(
+          *it,
+          from_integer(size - i - 1, index_type),
+          vector_type.element_type()));
 
       out << " ";
       convert_expr(tmp);
@@ -3839,7 +3840,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
     {
       // fixed-width
       std::size_t array_width=boolbv_width(array_type);
-      std::size_t sub_width=boolbv_width(array_type.subtype());
+      std::size_t sub_width = boolbv_width(array_type.element_type());
       std::size_t index_width=boolbv_width(expr.where().type());
 
       // We mask out the updated bits with AND,
@@ -4084,9 +4085,9 @@ void smt2_convt::convert_index(const index_exprt &expr)
       std::size_t array_width=boolbv_width(array_type);
       CHECK_RETURN(array_width != 0);
 
-      unflatten(wheret::BEGIN, array_type.subtype());
+      unflatten(wheret::BEGIN, array_type.element_type());
 
-      std::size_t sub_width=boolbv_width(array_type.subtype());
+      std::size_t sub_width = boolbv_width(array_type.element_type());
       std::size_t index_width=boolbv_width(expr.index().type());
 
       out << "((_ extract " << sub_width-1 << " 0) ";
@@ -4112,7 +4113,7 @@ void smt2_convt::convert_index(const index_exprt &expr)
 
       out << ")))"; // mult, bvlshr, extract
 
-      unflatten(wheret::END, array_type.subtype());
+      unflatten(wheret::END, array_type.element_type());
     }
   }
   else if(array_op_type.id()==ID_vector)
@@ -4318,7 +4319,7 @@ void smt2_convt::unflatten(
       // extract elements
       const vector_typet &vector_type=to_vector_type(type);
 
-      std::size_t subtype_width=boolbv_width(vector_type.subtype());
+      std::size_t subtype_width = boolbv_width(vector_type.element_type());
 
       mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
 
@@ -4335,10 +4336,10 @@ void smt2_convt::unflatten(
         for(mp_integer i=0; i!=size; ++i, offset+=subtype_width)
         {
           out << " ";
-          unflatten(wheret::BEGIN, vector_type.subtype(), nesting+1);
+          unflatten(wheret::BEGIN, vector_type.element_type(), nesting + 1);
           out << "((_ extract " << offset+subtype_width-1 << " "
               << offset << ") ?ufop" << nesting << ")";
-          unflatten(wheret::END, vector_type.subtype(), nesting+1);
+          unflatten(wheret::END, vector_type.element_type(), nesting + 1);
         }
 
         out << "))"; // mk-, let
@@ -4630,7 +4631,7 @@ void smt2_convt::find_symbols(const exprt &expr)
         out << "(assert (forall ((i ";
         convert_type(array_type.size().type());
         out << ")) (= (select " << id << " i) ";
-        if(array_type.subtype().id() == ID_bool && !use_array_of_bool)
+        if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
         {
           out << "(ite ";
           convert_expr(array_of.what());
@@ -4678,7 +4679,7 @@ void smt2_convt::find_symbols(const exprt &expr)
         out << ")) (= (select " << id << " ";
         convert_expr(array_comprehension.arg());
         out << ") ";
-        if(array_type.subtype().id() == ID_bool && !use_array_of_bool)
+        if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
         {
           out << "(ite ";
           convert_expr(array_comprehension.body());
@@ -4711,7 +4712,7 @@ void smt2_convt::find_symbols(const exprt &expr)
         out << "(assert (= (select " << id << " ";
         convert_expr(from_integer(i, array_type.size().type()));
         out << ") "; // select
-        if(array_type.subtype().id() == ID_bool && !use_array_of_bool)
+        if(array_type.element_type().id() == ID_bool && !use_array_of_bool)
         {
           out << "(ite ";
           convert_expr(expr.operands()[i]);
@@ -4865,7 +4866,7 @@ void smt2_convt::convert_type(const typet &type)
     CHECK_RETURN(array_type.size().is_not_nil());
 
     // we always use array theory for top-level arrays
-    const typet &subtype = array_type.subtype();
+    const typet &subtype = array_type.element_type();
 
     out << "(Array ";
     convert_type(array_type.size().type());
@@ -4874,7 +4875,7 @@ void smt2_convt::convert_type(const typet &type)
     if(subtype.id()==ID_bool && !use_array_of_bool)
       out << "(_ BitVec 1)";
     else
-      convert_type(array_type.subtype());
+      convert_type(array_type.element_type());
 
     out << ")";
   }
@@ -5008,7 +5009,7 @@ void smt2_convt::find_symbols_rec(
   {
     const array_typet &array_type=to_array_type(type);
     find_symbols(array_type.size());
-    find_symbols_rec(array_type.subtype(), recstack);
+    find_symbols_rec(array_type.element_type(), recstack);
   }
   else if(type.id()==ID_complex)
   {
diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index 838be81ebfd..0a8ffe1e922 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -26,7 +26,7 @@ std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
   {
     const auto &array_type = to_array_type(type);
     out << "(Array " << smt2_format(array_type.size().type()) << ' '
-        << smt2_format(array_type.subtype()) << ')';
+        << smt2_format(array_type.element_type()) << ')';
   }
   else if(type.id() == ID_floatbv)
   {
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
index 5e25ae6c45b..b4854c07b63 100644
--- a/src/solvers/smt2/smt2_parser.cpp
+++ b/src/solvers/smt2/smt2_parser.cpp
@@ -829,7 +829,7 @@ exprt smt2_parsert::function_application()
 
           auto value = expression();
 
-          if(value.type() != array_sort.subtype())
+          if(value.type() != array_sort.element_type())
             throw error() << "unexpected 'as const' with wrong element type";
 
           if(smt2_tokenizer.next_token() != smt2_tokenizert::CLOSE)
@@ -1215,7 +1215,7 @@ void smt2_parsert::setup_expressions()
     if(op[0].type().id() != ID_array)
       throw error("store expects array operand");
 
-    if(to_array_type(op[0].type()).subtype() != op[2].type())
+    if(to_array_type(op[0].type()).element_type() != op[2].type())
       throw error("store expects value that matches array element type");
 
     return with_exprt(op[0], op[1], op[2]);
diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp
index 7fa50dc4760..a97023d6a39 100644
--- a/src/solvers/strings/string_builtin_function.cpp
+++ b/src/solvers/strings/string_builtin_function.cpp
@@ -58,7 +58,7 @@ template <typename Iter>
 static array_string_exprt
 make_string(Iter begin, Iter end, const array_typet &array_type)
 {
-  const typet &char_type = array_type.subtype();
+  const typet &char_type = array_type.element_type();
   array_exprt array_expr({}, array_type);
   const auto &insert = std::back_inserter(array_expr.operands());
   std::transform(begin, end, insert, [&](const mp_integer &i) {
diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp
index d4010adc498..ab410637b47 100644
--- a/src/solvers/strings/string_format_builtin_function.cpp
+++ b/src/solvers/strings/string_format_builtin_function.cpp
@@ -242,7 +242,8 @@ static exprt format_arg_from_string(
   array_poolt &array_pool)
 {
   PRECONDITION(
-    to_array_type(string.content().type()).subtype() == unsignedbv_typet(16));
+    to_array_type(string.content().type()).element_type() ==
+    unsignedbv_typet(16));
 
   if(id == "string_expr")
     return string;
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index 773dda84eb0..dd281d35ad8 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -1170,7 +1170,7 @@ static exprt substitute_array_access(
   const exprt &index,
   symbol_generatort &symbol_generator)
 {
-  const typet &char_type = array_expr.type().subtype();
+  const typet &char_type = array_expr.type().element_type();
   const exprt default_val = symbol_generator("out_of_bound_access", char_type);
   const interval_sparse_arrayt sparse_array(array_expr, default_val);
   return sparse_array.to_if_expression(index);
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
index e7f883a7066..57749bd396c 100644
--- a/src/util/base_type.cpp
+++ b/src/util/base_type.cpp
@@ -70,7 +70,7 @@ void base_type_rec(
   }
   else if(type.id()==ID_array)
   {
-    base_type_rec(to_array_type(type).subtype(), ns, symb);
+    base_type_rec(to_array_type(type).element_type(), ns, symb);
   }
   else if(type.id()==ID_struct ||
           type.id()==ID_union)
@@ -233,7 +233,8 @@ bool base_type_eqt::base_type_eq_rec(
   else if(type1.id()==ID_array)
   {
     if(!base_type_eq_rec(
-      to_array_type(type1).subtype(), to_array_type(type2).subtype()))
+         to_array_type(type1).element_type(),
+         to_array_type(type2).element_type()))
       return false;
 
     if(to_array_type(type1).size()!=to_array_type(type2).size())
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
index 36f26ae4819..ea581ad374b 100644
--- a/src/util/endianness_map.cpp
+++ b/src/util/endianness_map.cpp
@@ -94,7 +94,7 @@ void endianness_mapt::build_big_endian(const typet &src)
     {
       while(*s > 0)
       {
-        build_big_endian(array_type.subtype());
+        build_big_endian(array_type.element_type());
         --(*s);
       }
     }
@@ -107,7 +107,7 @@ void endianness_mapt::build_big_endian(const typet &src)
 
     while(s > 0)
     {
-      build_big_endian(vector_type.subtype());
+      build_big_endian(vector_type.element_type());
       --s;
     }
   }
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index 6d80f3d1bd2..cc24fe0ce88 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -128,7 +128,8 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
     }
     else
     {
-      auto tmpval = expr_initializer_rec(array_type.subtype(), source_location);
+      auto tmpval =
+        expr_initializer_rec(array_type.element_type(), source_location);
       if(!tmpval.has_value())
         return {};
 
@@ -159,7 +160,8 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
   {
     const vector_typet &vector_type=to_vector_type(type);
 
-    auto tmpval = expr_initializer_rec(vector_type.subtype(), source_location);
+    auto tmpval =
+      expr_initializer_rec(vector_type.element_type(), source_location);
     if(!tmpval.has_value())
       return {};
 
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
index cca40c5b201..11560c150ad 100644
--- a/src/util/format_type.cpp
+++ b/src/util/format_type.cpp
@@ -68,9 +68,9 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
   {
     const auto &t = to_array_type(type);
     if(t.is_complete())
-      return os << format(t.subtype()) << '[' << format(t.size()) << ']';
+      return os << format(t.element_type()) << '[' << format(t.size()) << ']';
     else
-      return os << format(t.subtype()) << "[]";
+      return os << format(t.element_type()) << "[]";
   }
   else if(id == ID_struct)
     return format_rec(os, to_struct_type(type));
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index d6be1f65240..2c63c94bf7e 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -102,7 +102,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
 {
   if(type.id()==ID_array)
   {
-    auto sub = pointer_offset_bits(to_array_type(type).subtype(), ns);
+    auto sub = pointer_offset_bits(to_array_type(type).element_type(), ns);
     if(!sub.has_value())
       return {};
 
@@ -115,7 +115,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_vector)
   {
-    auto sub = pointer_offset_bits(to_vector_type(type).subtype(), ns);
+    auto sub = pointer_offset_bits(to_vector_type(type).element_type(), ns);
     if(!sub.has_value())
       return {};
 
@@ -283,7 +283,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
     const auto &array_type = to_array_type(type);
 
     // special-case arrays of bits
-    if(array_type.subtype().id() == ID_bool)
+    if(array_type.element_type().id() == ID_bool)
     {
       auto bits = pointer_offset_bits(array_type, ns);
 
@@ -291,7 +291,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
         return from_integer((*bits + 7) / 8, size_type());
     }
 
-    auto sub = size_of_expr(array_type.subtype(), ns);
+    auto sub = size_of_expr(array_type.element_type(), ns);
     if(!sub.has_value())
       return {};
 
@@ -310,7 +310,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
     const auto &vector_type = to_vector_type(type);
 
     // special-case vectors of bits
-    if(vector_type.subtype().id() == ID_bool)
+    if(vector_type.element_type().id() == ID_bool)
     {
       auto bits = pointer_offset_bits(vector_type, ns);
 
@@ -318,7 +318,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
         return from_integer((*bits + 7) / 8, size_type());
     }
 
-    auto sub = size_of_expr(vector_type.subtype(), ns);
+    auto sub = size_of_expr(vector_type.element_type(), ns);
     if(!sub.has_value())
       return {};
 
@@ -521,7 +521,7 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
     if(o.has_value())
     {
       const auto &array_type = to_array_type(index_expr.array().type());
-      auto sub_size = pointer_offset_size(array_type.subtype(), ns);
+      auto sub_size = pointer_offset_size(array_type.element_type(), ns);
 
       if(sub_size.has_value() && *sub_size > 0)
       {
@@ -660,7 +660,8 @@ optionalt<exprt> get_subexpression_at_offset(
   {
     const array_typet &array_type = to_array_type(source_type);
 
-    const auto elem_size_bits = pointer_offset_bits(array_type.subtype(), ns);
+    const auto elem_size_bits =
+      pointer_offset_bits(array_type.element_type(), ns);
 
     // no arrays of non-byte-aligned, zero-, or unknown-sized objects
     if(
diff --git a/src/util/refined_string_type.h b/src/util/refined_string_type.h
index 2fce2cc56a9..96b12923059 100644
--- a/src/util/refined_string_type.h
+++ b/src/util/refined_string_type.h
@@ -39,7 +39,7 @@ class refined_string_typet: public struct_typet
 
   const typet &get_char_type() const
   {
-    return get_content_type().subtype();
+    return get_content_type().element_type();
   }
 
   const typet &get_index_type() const
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 9afb82cc23d..a483a99f270 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1313,7 +1313,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     // turn &array into &array[0] when casting to pointer-to-element-type
     if(
       o.type().id() == ID_array &&
-      expr_type == pointer_type(o.type().subtype()))
+      expr_type == pointer_type(to_array_type(o.type()).element_type()))
     {
       auto result =
         address_of_exprt(index_exprt(o, from_integer(0, size_type())));
@@ -1374,7 +1374,7 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
         index_exprt idx(
           old.array(),
           pointer_offset_sum(old.index(), pointer_plus_expr.op1()),
-          old.array().type().subtype());
+          to_array_type(old.array().type()).element_type());
         return changed(simplify_rec(idx));
       }
     }
@@ -1967,7 +1967,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
       }
       else if(tp.id()==ID_array)
       {
-        auto i = pointer_offset_size(to_array_type(tp).subtype(), ns);
+        auto i = pointer_offset_size(to_array_type(tp).element_type(), ns);
         if(i.has_value())
         {
           const exprt &index=with.where();
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index e5a06d7e101..cfc48924b76 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -171,9 +171,9 @@ simplify_exprt::simplify_index(const index_exprt &expr)
     {
       optionalt<typet> subtype;
       if(array.type().id() == ID_array)
-        subtype = to_array_type(array.type()).subtype();
+        subtype = to_array_type(array.type()).element_type();
       else
-        subtype = to_vector_type(array.type()).subtype();
+        subtype = to_vector_type(array.type()).element_type();
 
       // This rewrites byte_extract(s, o, array_type)[i]
       // to byte_extract(s, o+offset, sub_type)
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index 3199a6cd57a..e58ab735eea 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -335,7 +335,7 @@ optionalt<exprt> bits2expr(
     const std::size_t number_of_elements =
       numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
 
-    const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns);
+    const auto el_size_opt = pointer_offset_bits(array_type.element_type(), ns);
     CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
 
     const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
@@ -346,7 +346,8 @@ optionalt<exprt> bits2expr(
     for(std::size_t i = 0; i < number_of_elements; ++i)
     {
       std::string el_bits = std::string(bits, i * el_size, el_size);
-      auto el = bits2expr(el_bits, array_type.subtype(), little_endian, ns);
+      auto el =
+        bits2expr(el_bits, array_type.element_type(), little_endian, ns);
       if(!el.has_value())
         return {};
       result.add_to_operands(std::move(*el));
@@ -360,7 +361,8 @@ optionalt<exprt> bits2expr(
 
     const std::size_t n_el = numeric_cast_v<std::size_t>(vector_type.size());
 
-    const auto el_size_opt = pointer_offset_bits(vector_type.subtype(), ns);
+    const auto el_size_opt =
+      pointer_offset_bits(vector_type.element_type(), ns);
     CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
 
     const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
@@ -371,7 +373,8 @@ optionalt<exprt> bits2expr(
     for(std::size_t i = 0; i < n_el; ++i)
     {
       std::string el_bits = std::string(bits, i * el_size, el_size);
-      auto el = bits2expr(el_bits, vector_type.subtype(), little_endian, ns);
+      auto el =
+        bits2expr(el_bits, vector_type.element_type(), little_endian, ns);
       if(!el.has_value())
         return {};
       result.add_to_operands(std::move(*el));
diff --git a/src/util/std_types.h b/src/util/std_types.h
index ec69e0ef298..399bcc538a9 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -779,6 +779,14 @@ class array_typet:public type_with_subtypet
     return subtype();
   }
 
+  /// The type of the elements of the array.
+  /// This method is preferred over .subtype(),
+  /// which will eventually be deprecated.
+  typet &element_type()
+  {
+    return subtype();
+  }
+
   const exprt &size() const
   {
     return static_cast<const exprt &>(find(ID_size));
@@ -998,6 +1006,14 @@ class vector_typet:public type_with_subtypet
     return subtype();
   }
 
+  /// The type of the elements of the vector.
+  /// This method is preferred over .subtype(),
+  /// which will eventually be deprecated.
+  typet &element_type()
+  {
+    return subtype();
+  }
+
   const constant_exprt &size() const;
   constant_exprt &size();
 };
diff --git a/src/util/string_constant.cpp b/src/util/string_constant.cpp
index 8b44cc1119f..9d2fa2c614a 100644
--- a/src/util/string_constant.cpp
+++ b/src/util/string_constant.cpp
@@ -30,7 +30,7 @@ array_exprt string_constantt::to_array_expr() const
 {
   const std::string &str=get_string(ID_value);
   std::size_t string_size=str.size()+1; // we add the zero
-  const typet &char_type = to_array_type(type()).subtype();
+  const typet &char_type = to_array_type(type()).element_type();
   bool char_is_unsigned=char_type.id()==ID_unsignedbv;
 
   exprt size = from_integer(string_size, c_index_type());