diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
index 5e73e6b4eff..0fbd027ffae 100644
--- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
+++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
@@ -174,7 +174,7 @@ void ci_lazy_methods_neededt::gather_field_types(
         gather_field_types(field.type(), ns);
       else if(field.type().id() == ID_pointer)
       {
-        if(field.type().subtype().id() == ID_struct_tag)
+        if(to_pointer_type(field.type()).base_type().id() == ID_struct_tag)
         {
           add_all_needed_classes(to_pointer_type(field.type()));
         }
@@ -186,7 +186,7 @@ void ci_lazy_methods_neededt::gather_field_types(
           // We should therefore only be skipping pointers such as the uint16t*
           // in our internal String representation.
           INVARIANT(
-            field.type().subtype().id() != ID_struct,
+            to_pointer_type(field.type()).base_type().id() != ID_struct,
             "struct types should be referred to by symbol at this stage");
         }
       }
diff --git a/jbmc/src/java_bytecode/convert_java_nondet.cpp b/jbmc/src/java_bytecode/convert_java_nondet.cpp
index 942014e2481..73cfbba2aab 100644
--- a/jbmc/src/java_bytecode/convert_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/convert_java_nondet.cpp
@@ -27,9 +27,10 @@ static bool is_nondet_pointer(exprt expr)
   // and we do not want to convert it. If the type is a ptr-to-void or a
   // function pointer then we also do not want to convert it.
   const typet &type = expr.type();
-  const bool non_void_non_function_pointer = type.id() == ID_pointer &&
-                                             type.subtype().id() != ID_empty &&
-                                             type.subtype().id() != ID_code;
+  const bool non_void_non_function_pointer =
+    type.id() == ID_pointer &&
+    to_pointer_type(type).base_type().id() != ID_empty &&
+    to_pointer_type(type).base_type().id() != ID_code;
   return can_cast_expr<side_effect_expr_nondett>(expr) &&
          non_void_non_function_pointer;
 }
diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp
index 59deccae7e9..bff889ab712 100644
--- a/jbmc/src/java_bytecode/expr2java.cpp
+++ b/jbmc/src/java_bytecode/expr2java.cpp
@@ -340,13 +340,13 @@ std::string expr2javat::convert_java_new(const exprt &src)
       convert(static_cast<const exprt &>(src.find(ID_size)));
 
     dest+=' ';
-    dest+=convert(src.type().subtype());
+    dest += convert(to_pointer_type(src.type()).base_type());
     dest+='[';
     dest+=tmp_size;
     dest+=']';
   }
   else
-    dest="new "+convert(src.type().subtype());
+    dest = "new " + convert(to_pointer_type(src.type()).base_type());
 
   return dest;
 }
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp
index 9e04c9684ce..cb593a66dbe 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp
@@ -102,7 +102,7 @@ java_bytecode_parse_treet::find_annotation(
     [&annotation_type_name](const annotationt &annotation) {
       if(annotation.type.id() != ID_pointer)
         return false;
-      const typet &type = annotation.type.subtype();
+      const typet &type = to_pointer_type(annotation.type).base_type();
       return type.id() == ID_struct_tag &&
              to_struct_tag_type(type).get_identifier() == annotation_type_name;
     });
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index c913ec2d426..dbb04f04732 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -600,7 +600,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
       get_class_refs_rec(c.type());
   }
   else if(src.id()==ID_pointer)
-    get_class_refs_rec(src.subtype());
+    get_class_refs_rec(to_pointer_type(src).base_type());
 }
 
 /// For each of the given annotations, get a reference to its class and
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 67a4643a214..4304d232734 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1381,16 +1381,16 @@ code_blockt gen_nondet_array_init(
   const size_t max_nondet_array_length)
 {
   PRECONDITION(expr.type().id() == ID_pointer);
-  PRECONDITION(expr.type().subtype().id() == ID_struct_tag);
+  PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_struct_tag);
   PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
 
   code_blockt statements;
 
   const namespacet ns(symbol_table);
-  const typet &type = ns.follow(expr.type().subtype());
+  const typet &type = ns.follow(to_pointer_type(expr.type()).base_type());
   const struct_typet &struct_type = to_struct_type(type);
-  const typet &element_type =
-    static_cast<const typet &>(expr.type().subtype().find(ID_element_type));
+  const typet &element_type = static_cast<const typet &>(
+    to_pointer_type(expr.type()).base_type().find(ID_element_type));
 
   auto max_length_expr = from_integer(max_nondet_array_length, java_int_type());
 
diff --git a/jbmc/src/java_bytecode/java_qualifiers.cpp b/jbmc/src/java_bytecode/java_qualifiers.cpp
index 5771aec0573..37b4b894b08 100644
--- a/jbmc/src/java_bytecode/java_qualifiers.cpp
+++ b/jbmc/src/java_bytecode/java_qualifiers.cpp
@@ -97,7 +97,9 @@ std::string java_qualifierst::as_string() const
   for(const java_annotationt &annotation : annotations)
   {
     out << '@';
-    out << annotation.get_type().subtype().get(ID_identifier);
+    out << to_reference_type(annotation.get_type())
+             .base_type()
+             .get(ID_identifier);
 
     if(!annotation.get_values().empty())
     {
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 8c303cd4bc1..a8ab53b4ea6 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -556,7 +556,8 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
   allocate_objectst allocate_objects(ID_java, loc, function_id, symbol_table);
 
   code_blockt tmp;
-  allocate_objects.allocate_dynamic_object(tmp, str, str.type().subtype());
+  allocate_objects.allocate_dynamic_object(
+    tmp, str, to_reference_type(str.type()).base_type());
   allocate_objects.declare_created_symbols(code);
   code.append(tmp);
 
diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp
index 48deaec0944..9d900444019 100644
--- a/jbmc/src/java_bytecode/lambda_synthesis.cpp
+++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp
@@ -586,7 +586,8 @@ static symbol_exprt instantiate_new_object(
     "REF_NewInvokeSpecial lambda must refer to a constructor");
   const auto &created_type = method_type.parameters().at(0).type();
   irep_idt created_class =
-    to_struct_tag_type(created_type.subtype()).get_identifier();
+    to_struct_tag_type(to_reference_type(created_type).base_type())
+      .get_identifier();
 
   // Call static init if it exists:
   irep_idt static_init_name = clinit_wrapper_name(created_class);
@@ -612,10 +613,11 @@ static symbol_exprt instantiate_new_object(
 
 /// If \p maybe_boxed_type is a boxed primitive return its unboxing method;
 /// otherwise return empty.
-static optionalt<irep_idt> get_unboxing_method(const typet &maybe_boxed_type)
+static optionalt<irep_idt>
+get_unboxing_method(const pointer_typet &maybe_boxed_type)
 {
   const irep_idt &boxed_type_id =
-    to_struct_tag_type(maybe_boxed_type.subtype()).get_identifier();
+    to_struct_tag_type(maybe_boxed_type.base_type()).get_identifier();
   const java_boxed_type_infot *boxed_type_info =
     get_boxed_type_info_by_name(boxed_type_id);
   return boxed_type_info ? boxed_type_info->unboxing_function_name
@@ -633,7 +635,8 @@ exprt make_function_expr(
   if(!method_type.has_this())
     return function_symbol.symbol_expr();
   const irep_idt &declared_on_class_id =
-    to_struct_tag_type(method_type.get_this()->type().subtype())
+    to_struct_tag_type(
+      to_pointer_type(method_type.get_this()->type()).base_type())
       .get_identifier();
   const auto &this_symbol = symbol_table.lookup_ref(declared_on_class_id);
   if(to_java_class_type(this_symbol.type).get_final())
@@ -717,7 +720,8 @@ exprt box_or_unbox_type_if_necessary(
 
   const irep_idt transform_function_id =
     original_is_pointer
-      ? get_unboxing_method(original_type) // Use static type if known
+      ? get_unboxing_method(
+          to_pointer_type(original_type)) // Use static type if known
           .value_or(primitive_type_info->unboxing_function_name)
       : primitive_type_info->boxed_type_factory_method;
 
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
index 06f3908e0c9..301bd8cd639 100644
--- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp
+++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp
@@ -99,7 +99,8 @@ void java_simple_method_stubst::create_method_stub_at(
 
   namespacet ns(symbol_table);
 
-  const auto &expected_base = ns.follow(expected_type.subtype());
+  const auto &expected_base =
+    ns.follow(to_pointer_type(expected_type).base_type());
   if(expected_base.id() != ID_struct)
     return;
 
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 607f02ee78b..40b4aa3c4ed 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -574,13 +574,13 @@ bool cpp_typecheckt::standard_conversion_pointer_to_member(
       to_pointer_type(type).base_type().id() == ID_code &&
       to_pointer_type(expr.type()).base_type().id() == ID_code)
     {
-      code_typet code1=to_code_type(expr.type().subtype());
+      code_typet code1 = to_code_type(to_pointer_type(expr.type()).base_type());
       assert(!code1.parameters().empty());
       code_typet::parametert this1=code1.parameters()[0];
       INVARIANT(this1.get_this(), "first parameter should be `this'");
       code1.parameters().erase(code1.parameters().begin());
 
-      code_typet code2=to_code_type(type.subtype());
+      code_typet code2 = to_code_type(to_pointer_type(type).base_type());
       assert(!code2.parameters().empty());
       code_typet::parametert this2=code2.parameters()[0];
       INVARIANT(this2.get_this(), "first parameter should be `this'");
@@ -1118,7 +1118,7 @@ bool cpp_typecheckt::reference_related(
   assert(!is_reference(expr.type()));
 
   typet from=follow(expr.type());
-  typet to=follow(type.subtype());
+  typet to = follow(to_reference_type(type).base_type());
 
   // need to check #c_type
   if(from.get(ID_C_c_type)!=to.get(ID_C_c_type))
@@ -1667,7 +1667,7 @@ bool cpp_typecheckt::const_typecast(
     if(!expr.get_bool(ID_C_lvalue))
       return false;
 
-    if(new_expr.type()!=type.subtype())
+    if(new_expr.type() != to_reference_type(type).base_type())
       return false;
 
     address_of_exprt address_of(expr, to_pointer_type(type));
@@ -1710,7 +1710,7 @@ bool cpp_typecheckt::dynamic_typecast(
 
   if(is_reference(type))
   {
-    if(type.subtype().id() != ID_struct_tag)
+    if(to_reference_type(type).base_type().id() != ID_struct_tag)
       return false;
   }
   else if(type.id()==ID_pointer)
@@ -1718,13 +1718,13 @@ bool cpp_typecheckt::dynamic_typecast(
     if(type.find(ID_to_member).is_not_nil())
       return false;
 
-    if(type.subtype().id()==ID_empty)
+    if(to_pointer_type(type).base_type().id() == ID_empty)
     {
       if(!e.get_bool(ID_C_lvalue))
         return false;
       UNREACHABLE; // currently not supported
     }
-    else if(type.subtype().id() == ID_struct_tag)
+    else if(to_pointer_type(type).base_type().id() == ID_struct_tag)
     {
       if(e.get_bool(ID_C_lvalue))
       {
@@ -1863,7 +1863,7 @@ bool cpp_typecheckt::static_typecast(
     if(reference_binding(e, type, new_expr, rank))
       return true;
 
-    typet subto=follow(type.subtype());
+    typet subto = follow(to_pointer_type(type).base_type());
     typet from=follow(e.type());
 
     if(subto.id()==ID_struct && from.id()==ID_struct)
@@ -1875,7 +1875,7 @@ bool cpp_typecheckt::static_typecast(
       qual_from.read(e.type());
 
       c_qualifierst qual_to;
-      qual_to.read(type.subtype());
+      qual_to.read(to_pointer_type(type).base_type());
 
       if(!qual_to.is_subset_of(qual_from))
         return false;
@@ -1945,8 +1945,8 @@ bool cpp_typecheckt::static_typecast(
   {
     if(type.find(ID_to_member).is_nil() && e.type().find(ID_to_member).is_nil())
     {
-      typet to=follow(type.subtype());
-      typet from=follow(e.type().subtype());
+      typet to = follow(to_pointer_type(type).base_type());
+      typet from = follow(to_pointer_type(e.type()).base_type());
 
       if(from.id()==ID_empty)
       {
@@ -1979,7 +1979,9 @@ bool cpp_typecheckt::static_typecast(
       type.find(ID_to_member).is_not_nil() &&
       e.type().find(ID_to_member).is_not_nil())
     {
-      if(type.subtype()!=e.type().subtype())
+      if(
+        to_pointer_type(type).base_type() !=
+        to_pointer_type(e.type()).base_type())
         return false;
 
       const struct_typet &from_struct = to_struct_type(
@@ -1998,8 +2000,12 @@ bool cpp_typecheckt::static_typecast(
       type.find(ID_to_member).is_nil() &&
       e.type().find(ID_to_member).is_not_nil())
     {
-      if(type.subtype() != e.type().subtype())
+      if(
+        to_pointer_type(type).base_type() !=
+        to_pointer_type(e.type()).base_type())
+      {
         return false;
+      }
 
       const struct_typet &from_struct = to_struct_type(
         follow(static_cast<const typet &>(e.type().find(ID_to_member))));
diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp
index 545ff08f7e9..34d9fe4fbdb 100644
--- a/src/cpp/expr2cpp.cpp
+++ b/src/cpp/expr2cpp.cpp
@@ -258,7 +258,9 @@ std::string expr2cppt::convert_rec(
     dest += "> " + convert(to_template_type(src).subtype());
     return dest;
   }
-  else if(src.id()==ID_pointer && src.subtype().id()==ID_nullptr)
+  else if(
+    src.id() == ID_pointer &&
+    to_pointer_type(src).base_type().id() == ID_nullptr)
   {
     return "std::nullptr_t";
   }
@@ -270,9 +272,11 @@ std::string expr2cppt::convert_rec(
 
     std::string dest="("+convert_rec(member, c_qualifierst(), "")+":: *)";
 
-    if(src.subtype().id()==ID_code)
+    const auto &base_type = to_pointer_type(src).base_type();
+
+    if(base_type.id() == ID_code)
     {
-      const code_typet &code_type = to_code_type(src.subtype());
+      const code_typet &code_type = to_code_type(base_type);
       const typet &return_type = code_type.return_type();
       dest=convert_rec(return_type, c_qualifierst(), "")+" "+dest;
 
@@ -292,7 +296,7 @@ std::string expr2cppt::convert_rec(
       dest+=d;
     }
     else
-      dest=convert_rec(src.subtype(), c_qualifierst(), "")+" "+dest+d;
+      dest = convert_rec(base_type, c_qualifierst(), "") + " " + dest + d;
 
     return dest;
   }
@@ -375,13 +379,13 @@ std::string expr2cppt::convert_cpp_new(const exprt &src)
       convert(static_cast<const exprt &>(src.find(ID_size)));
 
     dest+=' ';
-    dest+=convert(src.type().subtype());
+    dest += convert(to_pointer_type(src.type()).base_type());
     dest+='[';
     dest+=tmp_size;
     dest+=']';
   }
   else
-    dest="new "+convert(src.type().subtype());
+    dest = "new " + convert(to_pointer_type(src.type()).base_type());
 
   return dest;
 }
diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp
index a494897fa1f..715991ceda5 100644
--- a/src/goto-harness/memory_snapshot_harness_generator.cpp
+++ b/src/goto-harness/memory_snapshot_harness_generator.cpp
@@ -201,7 +201,7 @@ size_t memory_snapshot_harness_generatort::pointer_depth(const typet &t) const
   if(t.id() != ID_pointer)
     return 0;
   else
-    return pointer_depth(t.subtype()) + 1;
+    return pointer_depth(to_pointer_type(t).base_type()) + 1;
 }
 
 code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp
index 1a79b787da4..32deef9090f 100644
--- a/src/goto-harness/recursive_initialization.cpp
+++ b/src/goto-harness/recursive_initialization.cpp
@@ -235,7 +235,8 @@ void recursive_initializationt::initialize(
 
 code_blockt build_null_pointer(const symbol_exprt &result_symbol)
 {
-  const typet &type_to_construct = result_symbol.type().subtype();
+  const typet &type_to_construct =
+    to_pointer_type(result_symbol.type()).base_type();
   const null_pointer_exprt nullptr_expr{to_pointer_type(type_to_construct)};
   const code_assignt assign_null{dereference_exprt{result_symbol},
                                  nullptr_expr};
@@ -250,18 +251,18 @@ code_blockt recursive_initializationt::build_constructor_body(
   const bool is_nullable)
 {
   PRECONDITION(result_symbol.type().id() == ID_pointer);
-  const typet &type = result_symbol.type().subtype();
+  const typet &type = to_pointer_type(result_symbol.type()).base_type();
   if(type.id() == ID_struct_tag)
   {
     return build_struct_constructor(depth_symbol, result_symbol);
   }
   else if(type.id() == ID_pointer)
   {
-    if(type.subtype().id() == ID_code)
+    if(to_pointer_type(type).base_type().id() == ID_code)
     {
       return build_function_pointer_constructor(result_symbol, is_nullable);
     }
-    if(type.subtype().id() == ID_empty)
+    if(to_pointer_type(type).base_type().id() == ID_empty)
     {
       // always initalize void* pointers as NULL
       return build_null_pointer(result_symbol);
@@ -610,12 +611,13 @@ std::string recursive_initializationt::type2id(const typet &type) const
     return st_tag;
   }
   else if(type.id() == ID_pointer)
-    return "ptr_" + type2id(type.subtype());
+    return "ptr_" + type2id(to_pointer_type(type).base_type());
   else if(type.id() == ID_array)
   {
     const auto array_size =
       numeric_cast_v<std::size_t>(to_constant_expr(to_array_type(type).size()));
-    return "arr_" + type2id(type.subtype()) + "_" + std::to_string(array_size);
+    return "arr_" + type2id(to_array_type(type).element_type()) + "_" +
+           std::to_string(array_size);
   }
   else if(type == char_type())
     return "char";
@@ -649,9 +651,9 @@ code_blockt recursive_initializationt::build_pointer_constructor(
   const symbol_exprt &result)
 {
   PRECONDITION(result.type().id() == ID_pointer);
-  const typet &type = result.type().subtype();
+  const typet &type = to_pointer_type(result.type()).base_type();
   PRECONDITION(type.id() == ID_pointer);
-  PRECONDITION(type.subtype().id() != ID_empty);
+  PRECONDITION(to_pointer_type(type).base_type().id() != ID_empty);
 
   code_blockt body{};
   // build:
@@ -677,8 +679,9 @@ code_blockt recursive_initializationt::build_pointer_constructor(
   exprt::operandst should_not_recurse{depth_gt_max_depth};
 
   optionalt<symbol_exprt> has_seen;
-  if(can_cast_type<struct_tag_typet>(type.subtype()))
-    has_seen = get_fresh_global_symexpr("has_seen_" + type2id(type.subtype()));
+  if(can_cast_type<struct_tag_typet>(to_pointer_type(type).base_type()))
+    has_seen = get_fresh_global_symexpr(
+      "has_seen_" + type2id(to_pointer_type(type).base_type()));
 
   if(has_seen.has_value())
   {
@@ -686,7 +689,8 @@ code_blockt recursive_initializationt::build_pointer_constructor(
     should_not_recurse.push_back(has_seen_expr);
   }
 
-  null_pointer_exprt nullptr_expr{pointer_type(type.subtype())};
+  null_pointer_exprt nullptr_expr{
+    pointer_type(to_pointer_type(type).base_type())};
   const code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
   code_blockt null_and_return{{assign_null, code_frontend_returnt{}}};
   body.add(code_ifthenelset{conjunction(should_not_recurse), null_and_return});
@@ -702,8 +706,8 @@ code_blockt recursive_initializationt::build_pointer_constructor(
   code_assignt seen_assign_prev{};
   if(has_seen.has_value())
   {
-    const symbol_exprt &has_seen_prev =
-      get_fresh_local_symexpr("has_seen_prev_" + type2id(type.subtype()));
+    const symbol_exprt &has_seen_prev = get_fresh_local_symexpr(
+      "has_seen_prev_" + type2id(to_pointer_type(type).base_type()));
     then_case.add(code_declt{has_seen_prev});
     then_case.add(code_assignt{has_seen_prev, *has_seen});
     then_case.add(code_assignt{*has_seen, from_integer(1, has_seen->type())});
@@ -711,17 +715,17 @@ code_blockt recursive_initializationt::build_pointer_constructor(
   }
 
   // we want to initialize the pointee as non-const even for pointer to const
-  const typet non_const_pointer_type =
-    pointer_type(remove_const(type.subtype()));
+  const pointer_typet non_const_pointer_type =
+    pointer_type(remove_const(to_pointer_type(type).base_type()));
   const symbol_exprt &local_result =
     get_fresh_local_typed_symexpr("local_result", non_const_pointer_type);
 
   then_case.add(code_declt{local_result});
   const namespacet ns{goto_model.symbol_table};
-  then_case.add(
-    code_function_callt{local_result,
-                        get_malloc_function(),
-                        {*size_of_expr(non_const_pointer_type.subtype(), ns)}});
+  then_case.add(code_function_callt{
+    local_result,
+    get_malloc_function(),
+    {*size_of_expr(non_const_pointer_type.base_type(), ns)}});
   initialize(
     dereference_exprt{local_result},
     plus_exprt{depth, from_integer(1, depth.type())},
@@ -743,7 +747,7 @@ code_blockt recursive_initializationt::build_array_constructor(
   const symbol_exprt &result)
 {
   PRECONDITION(result.type().id() == ID_pointer);
-  const typet &type = result.type().subtype();
+  const typet &type = to_pointer_type(result.type()).base_type();
   PRECONDITION(type.id() == ID_array);
   const array_typet &array_type = to_array_type(type);
   const auto array_size =
@@ -765,7 +769,7 @@ code_blockt recursive_initializationt::build_struct_constructor(
   const symbol_exprt &result)
 {
   PRECONDITION(result.type().id() == ID_pointer);
-  const typet &struct_type = result.type().subtype();
+  const typet &struct_type = to_pointer_type(result.type()).base_type();
   PRECONDITION(struct_type.id() == ID_struct_tag);
   code_blockt body{};
   const namespacet ns{goto_model.symbol_table};
@@ -803,8 +807,8 @@ code_blockt recursive_initializationt::build_nondet_constructor(
 {
   PRECONDITION(result.type().id() == ID_pointer);
   code_blockt body{};
-  auto const nondet_symbol =
-    get_fresh_local_typed_symexpr("nondet", result.type().subtype());
+  auto const nondet_symbol = get_fresh_local_typed_symexpr(
+    "nondet", to_pointer_type(result.type()).base_type());
   body.add(code_declt{nondet_symbol});
   body.add(code_assignt{dereference_exprt{result}, nondet_symbol});
   return body;
@@ -817,9 +821,9 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
   const optionalt<irep_idt> &lhs_name)
 {
   PRECONDITION(result.type().id() == ID_pointer);
-  const typet &dynamic_array_type = result.type().subtype();
+  const typet &dynamic_array_type = to_pointer_type(result.type()).base_type();
   PRECONDITION(dynamic_array_type.id() == ID_pointer);
-  const typet &element_type = dynamic_array_type.subtype();
+  const typet &element_type = to_pointer_type(dynamic_array_type).base_type();
   PRECONDITION(element_type.id() != ID_empty);
 
   // builds:
@@ -911,14 +915,17 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
     notequal_exprt{size, null_pointer_exprt{to_pointer_type(size.type())}},
     code_assignt{
       dereference_exprt{size},
-      typecast_exprt::conditional_cast(nondet_size, size.type().subtype())}});
+      typecast_exprt::conditional_cast(
+        nondet_size, to_pointer_type(size.type()).base_type())}});
 
   return body;
 }
 
 bool recursive_initializationt::needs_freeing(const exprt &expr) const
 {
-  if(expr.type().id() != ID_pointer || expr.type().subtype().id() == ID_code)
+  if(
+    expr.type().id() != ID_pointer ||
+    to_pointer_type(expr.type()).base_type().id() == ID_code)
     return false;
   for(auto const &common_arguments_origin : common_arguments_origins)
   {
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
index c02df30cd13..100aa91d435 100644
--- a/src/goto-programs/string_instrumentation.cpp
+++ b/src/goto-programs/string_instrumentation.cpp
@@ -882,10 +882,11 @@ void string_instrumentationt::invalidate_buffer(
   check->complete_goto(exit);
 
   const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
-  const dereference_exprt deref(b_plus_i, buf_type.subtype());
+  const dereference_exprt deref(
+    b_plus_i, to_type_with_subtype(buf_type).subtype());
 
   const side_effect_expr_nondett nondet(
-    buf_type.subtype(), target->source_location());
+    to_type_with_subtype(buf_type).subtype(), target->source_location());
 
   invalidate->code_nonconst() = code_assignt(deref, nondet);
 }
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 0fbf1676605..08fe2023242 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -781,9 +781,12 @@ void value_set_fit::get_reference_set_sharing_rec(
           expr.id()==ID_dynamic_object ||
           expr.id()==ID_string_constant)
   {
-    if(expr.type().id()==ID_array &&
-       expr.type().subtype().id()==ID_array)
+    if(
+      expr.type().id() == ID_array &&
+      to_array_type(expr.type()).element_type().id() == ID_array)
+    {
       insert(dest, expr);
+    }
     else
       insert(dest, expr, mp_integer{0});
 
@@ -1046,12 +1049,15 @@ void value_set_fit::assign(
   else if(type.id()==ID_array)
   {
     const index_exprt lhs_index(
-      lhs, exprt(ID_unknown, c_index_type()), type.subtype());
+      lhs,
+      exprt(ID_unknown, c_index_type()),
+      to_array_type(type).element_type());
 
     if(rhs.id()==ID_unknown ||
        rhs.id()==ID_invalid)
     {
-      assign(lhs_index, exprt(rhs.id(), type.subtype()), ns);
+      assign(
+        lhs_index, exprt(rhs.id(), to_array_type(type).element_type()), ns);
     }
     else if(rhs.is_nil())
     {