diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp
index 783b51dd1ef..83a937baf89 100644
--- a/jbmc/src/java_bytecode/assignments_from_json.cpp
+++ b/jbmc/src/java_bytecode/assignments_from_json.cpp
@@ -66,8 +66,8 @@ static java_class_typet
 followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
 {
   const pointer_typet &pointer_type = to_pointer_type(expr.type());
-  const java_class_typet &java_class_type =
-    to_java_class_type(namespacet{symbol_table}.follow(pointer_type.subtype()));
+  const java_class_typet &java_class_type = to_java_class_type(
+    namespacet{symbol_table}.follow(pointer_type.base_type()));
   return java_class_type;
 }
 
@@ -602,7 +602,7 @@ static code_with_references_listt assign_non_enum_pointer_from_json(
   code_blockt output_code;
   exprt dereferenced_symbol_expr =
     info.allocate_objects.allocate_dynamic_object(
-      output_code, expr, to_pointer_type(expr.type()).subtype());
+      output_code, expr, to_pointer_type(expr.type()).base_type());
   for(codet &code : output_code.statements())
     result.add(std::move(code));
   result.append(assign_struct_from_json(dereferenced_symbol_expr, json, info));
@@ -754,7 +754,7 @@ static get_or_create_reference_resultt get_or_create_reference(
     {
       code_blockt block;
       reference.expr = info.allocate_objects.allocate_dynamic_object_symbol(
-        block, expr, pointer_type.subtype());
+        block, expr, pointer_type.base_type());
       code.add(block);
     }
     auto iterator_inserted_pair = info.references.insert({id, reference});
diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
index 91b2bc21f58..5e73e6b4eff 100644
--- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
+++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
@@ -117,14 +117,14 @@ void ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer(
   const pointer_typet &pointer_type,
   const namespacet &ns)
 {
-  const auto &class_type = to_struct_tag_type(pointer_type.subtype());
+  const auto &class_type = to_struct_tag_type(pointer_type.base_type());
   const auto &param_classid = class_type.get_identifier();
 
   // Note here: different arrays may have different element types, so we should
   // explore again even if we've seen this classid before in the array case.
   if(add_needed_class(param_classid) || is_java_array_tag(param_classid))
   {
-    gather_field_types(pointer_type.subtype(), ns);
+    gather_field_types(pointer_type.base_type(), ns);
   }
 
   if(is_java_generic_type(pointer_type))
@@ -159,7 +159,7 @@ void ci_lazy_methods_neededt::gather_field_types(
         java_array_element_type(to_struct_tag_type(class_type));
       if(
         element_type.id() == ID_pointer &&
-        element_type.subtype().id() != ID_empty)
+        to_pointer_type(element_type).base_type().id() != ID_empty)
       {
         // This is a reference array -- mark its element type available.
         add_all_needed_classes(to_pointer_type(element_type));
diff --git a/jbmc/src/java_bytecode/code_with_references.cpp b/jbmc/src/java_bytecode/code_with_references.cpp
index 3b74fa1da51..7bc38bab3f7 100644
--- a/jbmc/src/java_bytecode/code_with_references.cpp
+++ b/jbmc/src/java_bytecode/code_with_references.cpp
@@ -20,8 +20,8 @@ codet allocate_array(
 {
   pointer_typet pointer_type = to_pointer_type(expr.type());
   const auto &element_type =
-    java_array_element_type(to_struct_tag_type(pointer_type.subtype()));
-  pointer_type.subtype().set(ID_element_type, element_type);
+    java_array_element_type(to_struct_tag_type(pointer_type.base_type()));
+  pointer_type.base_type().set(ID_element_type, element_type);
   side_effect_exprt java_new_array{
     ID_java_new_array, {array_length_expr}, pointer_type, loc};
   return code_frontend_assignt{expr, java_new_array, loc};
diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp
index 33a58b78099..c7f786f4d58 100644
--- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp
+++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp
@@ -18,7 +18,7 @@ void generic_parameter_specialization_map_keyst::insert(
     return;
   // The supplied type must be the full type of the pointer's subtype
   PRECONDITION(
-    pointer_type.subtype().get(ID_identifier) ==
+    pointer_type.base_type().get(ID_identifier) ==
     pointer_subtype_struct.get(ID_name));
 
   // If the pointer points to:
diff --git a/jbmc/src/java_bytecode/goto_check_java.cpp b/jbmc/src/java_bytecode/goto_check_java.cpp
index 76eb7816abf..ebc9a56ace0 100644
--- a/jbmc/src/java_bytecode/goto_check_java.cpp
+++ b/jbmc/src/java_bytecode/goto_check_java.cpp
@@ -1148,7 +1148,7 @@ bool goto_check_javat::check_rec_member(const member_exprt &member)
   if(member_offset_opt.has_value())
   {
     pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
-    new_pointer_type.subtype() = member.type();
+    new_pointer_type.base_type() = member.type();
 
     const exprt char_pointer = typecast_exprt::conditional_cast(
       deref.pointer(), pointer_type(char_type()));
diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
index 9c6884834a7..cc5168eb627 100644
--- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -412,7 +412,7 @@ static void instrument_get_monitor_count(
 
   const namespacet ns(symbol_table);
   const auto &followed_type =
-    ns.follow(to_pointer_type(f_code.arguments()[0].type()).subtype());
+    ns.follow(to_pointer_type(f_code.arguments()[0].type()).base_type());
   const auto &object_type = to_struct_type(followed_type);
   code_assignt code_assign(
     f_code.lhs(),
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index fbad011e704..e58d844f3da 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -1235,7 +1235,7 @@ void mark_java_implicitly_generic_class_type(
                                 id2string(strip_java_namespace_prefix(
                                   outer_generic_type_parameter.get_name()));
           java_generic_parameter_tagt bound = to_java_generic_parameter_tag(
-            outer_generic_type_parameter.subtype());
+            outer_generic_type_parameter.base_type());
           bound.type_variable_ref().set_identifier(identifier);
           implicit_generic_type_parameters.emplace_back(identifier, bound);
         }
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index c68372823e8..3b505b068c9 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -2711,10 +2711,10 @@ void java_bytecode_convert_methodt::convert_getstatic(
     else if(arg0.type().id() == ID_pointer)
     {
       const auto &pointer_type = to_pointer_type(arg0.type());
-      if(pointer_type.subtype().id() == ID_struct_tag)
+      if(pointer_type.base_type().id() == ID_struct_tag)
       {
         needed_lazy_methods->add_needed_class(
-          to_struct_tag_type(pointer_type.subtype()).get_identifier());
+          to_struct_tag_type(pointer_type.base_type()).get_identifier());
       }
     }
     else if(is_assertions_disabled_field)
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index de056377e0c..65a4c8aac09 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -1486,7 +1486,7 @@ bool java_bytecode_languaget::convert_single_method_code(
       // TODO(tkiley): investigation
       namespacet ns{symbol_table};
       const java_class_typet &underlying_type =
-        to_java_class_type(ns.follow(pointer_return_type->subtype()));
+        to_java_class_type(ns.follow(pointer_return_type->base_type()));
 
       if(!underlying_type.is_abstract())
         needed_lazy_methods->add_all_needed_classes(*pointer_return_type);
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index ce7df5cfa16..54ebc3aeced 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -480,7 +480,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   const namespacet ns(symbol_table);
-  const typet &subtype = pointer_type.subtype();
+  const typet &subtype = pointer_type.base_type();
   const typet &followed_subtype = ns.follow(subtype);
   PRECONDITION(followed_subtype.id() == ID_struct);
   const pointer_typet &replacement_pointer_type =
@@ -499,7 +499,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
       generic_parameter_specialization_map_keys(
         generic_parameter_specialization_map);
     generic_parameter_specialization_map_keys.insert(
-      replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
+      replacement_pointer_type,
+      ns.follow(replacement_pointer_type.base_type()));
 
     const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
       assignments, lifetime, replacement_pointer_type, depth, location);
@@ -1019,7 +1020,7 @@ void java_object_factoryt::gen_nondet_init(
       generic_parameter_specialization_map_keys(
         generic_parameter_specialization_map);
     generic_parameter_specialization_map_keys.insert(
-      pointer_type, ns.follow(pointer_type.subtype()));
+      pointer_type, ns.follow(pointer_type.base_type()));
 
     gen_nondet_pointer_init(
       assignments,
diff --git a/jbmc/src/java_bytecode/java_pointer_casts.cpp b/jbmc/src/java_bytecode/java_pointer_casts.cpp
index 7dce1a3b524..0d5fe73ecbb 100644
--- a/jbmc/src/java_bytecode/java_pointer_casts.cpp
+++ b/jbmc/src/java_bytecode/java_pointer_casts.cpp
@@ -82,11 +82,13 @@ exprt make_clean_pointer_cast(
     return ptr;
 
   if(
-    ptr.type().subtype() == java_void_type() ||
-    target_type.subtype() == java_void_type())
+    to_pointer_type(ptr.type()).base_type() == java_void_type() ||
+    target_type.base_type() == java_void_type())
+  {
     return typecast_exprt(ptr, target_type);
+  }
 
-  const typet &target_base=ns.follow(target_type.subtype());
+  const typet &target_base = ns.follow(target_type.base_type());
 
   exprt bare_ptr=ptr;
   while(bare_ptr.id()==ID_typecast)
@@ -94,7 +96,7 @@ exprt make_clean_pointer_cast(
     assert(
       bare_ptr.type().id()==ID_pointer &&
       "Non-pointer in make_clean_pointer_cast?");
-    if(bare_ptr.type().subtype() == java_void_type())
+    if(to_pointer_type(bare_ptr.type()).base_type() == java_void_type())
       bare_ptr = to_typecast_expr(bare_ptr).op();
   }
 
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 18805b5496d..8c303cd4bc1 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -64,8 +64,8 @@ bool java_string_library_preprocesst::is_java_string_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_string_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_string_type(base_type);
   }
   return false;
 }
@@ -95,8 +95,8 @@ bool java_string_library_preprocesst::is_java_string_builder_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_string_builder_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_string_builder_type(base_type);
   }
   return false;
 }
@@ -118,8 +118,8 @@ bool java_string_library_preprocesst::is_java_string_buffer_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_string_buffer_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_string_buffer_type(base_type);
   }
   return false;
 }
@@ -141,8 +141,8 @@ bool java_string_library_preprocesst::is_java_char_sequence_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_char_sequence_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_char_sequence_type(base_type);
   }
   return false;
 }
@@ -164,8 +164,8 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type(
   if(type.id()==ID_pointer)
   {
     const pointer_typet &pt=to_pointer_type(type);
-    const typet &subtype=pt.subtype();
-    return is_java_char_array_type(subtype);
+    const typet &base_type = pt.base_type();
+    return is_java_char_array_type(base_type);
   }
   return false;
 }
diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
index 82f647ac453..72bed7ca73f 100644
--- a/jbmc/src/java_bytecode/java_types.cpp
+++ b/jbmc/src/java_bytecode/java_types.cpp
@@ -1049,9 +1049,9 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet(
   const java_generic_typet &gen_base_type = to_java_generic_type(*base_type);
   INVARIANT(
     type.get_identifier() ==
-      to_struct_tag_type(gen_base_type.subtype()).get_identifier(),
+      to_struct_tag_type(gen_base_type.base_type()).get_identifier(),
     "identifier of " + type.pretty() + "\n and identifier of type " +
-      gen_base_type.subtype().pretty() +
+      gen_base_type.base_type().pretty() +
       "\ncreated by java_type_from_string for " + base_ref +
       " should be equal");
   generic_types().insert(
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index a2b3fdbe2a4..1258c8fe44d 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -1056,7 +1056,7 @@ inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
   PRECONDITION(index<gen_types.size());
   const java_generic_parametert &gen_type=gen_types[index];
 
-  return gen_type.subtype();
+  return gen_type.base_type();
 }
 
 /// Type to hold a Java class that is implicitly generic, e.g., an inner
diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp
index 4964e4f01bb..f4d15127ec5 100644
--- a/jbmc/src/java_bytecode/java_utils.cpp
+++ b/jbmc/src/java_bytecode/java_utils.cpp
@@ -273,7 +273,7 @@ pointer_typet pointer_to_replacement_type(
   const pointer_typet &given_pointer_type,
   const java_class_typet &replacement_class_type)
 {
-  if(can_cast_type<struct_tag_typet>(given_pointer_type.subtype()))
+  if(can_cast_type<struct_tag_typet>(given_pointer_type.base_type()))
   {
     struct_tag_typet struct_tag_subtype{replacement_class_type.get_name()};
     return pointer_type(struct_tag_subtype);
diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index c485b6be01e..154d3133d97 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -59,13 +59,13 @@ pointer_typet select_pointer_typet::specialize_generics(
     }
   }
 
-  auto subtype =
-    type_try_dynamic_cast<struct_tag_typet>(pointer_type.subtype());
-  if(subtype != nullptr && is_java_array_tag(subtype->get_identifier()))
+  auto base_type =
+    type_try_dynamic_cast<struct_tag_typet>(pointer_type.base_type());
+  if(base_type != nullptr && is_java_array_tag(base_type->get_identifier()))
   {
     // if the pointer is an array, recursively specialize its element type
     const auto *array_element_type =
-      type_try_dynamic_cast<pointer_typet>(java_array_element_type(*subtype));
+      type_try_dynamic_cast<pointer_typet>(java_array_element_type(*base_type));
     if(array_element_type == nullptr)
       return pointer_type;
 
@@ -73,7 +73,7 @@ pointer_typet select_pointer_typet::specialize_generics(
       *array_element_type, generic_parameter_specialization_map);
 
     pointer_typet replacement_array_type = java_array_type('a');
-    replacement_array_type.subtype().set(ID_element_type, new_array_type);
+    replacement_array_type.base_type().set(ID_element_type, new_array_type);
     return replacement_array_type;
   }
 
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
index c5da0a39716..849d8861d2f 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
@@ -319,7 +319,7 @@ SCENARIO(
         // Trace the assignments back to the declaration of the generic type
         // and verify that it is what we expect.
         const auto &tmp_object_struct_tag = to_struct_tag_type(
-          to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
+          to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
         REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper");
 
         THEN("Object 'v' has field 'field' of type IWrapper")
@@ -369,7 +369,7 @@ SCENARIO(
         // Trace the assignments back to the declaration of the generic type
         // and verify that it is what we expect.
         const auto &tmp_object_struct_tag = to_struct_tag_type(
-          to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
+          to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
         REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper");
 
         THEN(
@@ -419,7 +419,7 @@ SCENARIO(
         // Trace the assignments back to the declaration of the generic type
         // and verify that it is what we expect.
         const auto &tmp_object_struct_tag = to_struct_tag_type(
-          to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
+          to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
         REQUIRE(
           tmp_object_struct_tag.get_identifier() ==
           "java::GenericFields$GenericInnerOuter$Outer");
@@ -484,7 +484,7 @@ SCENARIO(
         // Trace the assignments back to the declaration of the generic type
         // and verify that it is what we expect.
         const auto &tmp_object_struct_tag = to_struct_tag_type(
-          to_pointer_type(tmp_object_declaration.symbol().type()).subtype());
+          to_pointer_type(tmp_object_declaration.symbol().type()).base_type());
         REQUIRE(
           tmp_object_struct_tag.get_identifier() ==
           "java::GenericFields$GenericRewriteParameter$A");
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
index 12937b8d43d..9d49647a013 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
@@ -48,7 +48,7 @@ SCENARIO(
          {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}});
 
     // ... which is of type `KeyValue` ...
-    const auto &subtype = gen_type.subtype();
+    const auto &subtype = gen_type.base_type();
     const auto &key_value =
       symbol_table.lookup_ref(to_struct_tag_type(subtype).get_identifier());
     REQUIRE(key_value.type.id() == ID_struct);
@@ -66,9 +66,9 @@ SCENARIO(
         next.type(),
         {{require_type::type_argument_kindt::Var, "java::KeyValue::K"},
          {require_type::type_argument_kindt::Var, "java::KeyValue::V"}});
-    REQUIRE(next_type.subtype().id() == ID_struct_tag);
+    REQUIRE(next_type.base_type().id() == ID_struct_tag);
     const struct_tag_typet &next_symbol =
-      to_struct_tag_type(next_type.subtype());
+      to_struct_tag_type(next_type.base_type());
     REQUIRE(
       symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
       "java::KeyValue");
@@ -79,9 +79,9 @@ SCENARIO(
         reverse.type(),
         {{require_type::type_argument_kindt::Var, "java::KeyValue::V"},
          {require_type::type_argument_kindt::Var, "java::KeyValue::K"}});
-    REQUIRE(reverse_type.subtype().id() == ID_struct_tag);
+    REQUIRE(reverse_type.base_type().id() == ID_struct_tag);
     const struct_tag_typet &reverse_symbol =
-      to_struct_tag_type(reverse_type.subtype());
+      to_struct_tag_type(reverse_type.base_type());
     REQUIRE(
       symbol_table.lookup_ref(reverse_symbol.get_identifier()).name ==
       "java::KeyValue");
diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp
index 9610f0722f7..49cd0a3ba9b 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp
@@ -72,7 +72,7 @@ void validate_lambda_assignment(
     require_type::require_pointer(side_effect_expr.type(), {});
 
   const struct_tag_typet &lambda_implementor_type =
-    require_type::require_struct_tag(lambda_temp_type.subtype());
+    require_type::require_struct_tag(lambda_temp_type.base_type());
 
   const irep_idt &tmp_class_identifier =
     lambda_implementor_type.get_identifier();
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
index 9bf18e7729b..1d1fed7828f 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp
@@ -37,7 +37,7 @@ SCENARIO(
           field_t.type(), JAVA_REFERENCE_ARRAY_CLASSID);
 
       const struct_tag_typet &field_t_subtype =
-        to_struct_tag_type(field_t_pointer.subtype());
+        to_struct_tag_type(field_t_pointer.base_type());
       const struct_typet &subtype_type = to_struct_type(
         new_symbol_table.lookup_ref(field_t_subtype.get_identifier()).type);
       REQUIRE(is_valid_java_array(subtype_type));
@@ -63,7 +63,7 @@ SCENARIO(
           field_t2.type(), JAVA_REFERENCE_ARRAY_CLASSID);
 
       const struct_tag_typet &field_t2_subtype =
-        to_struct_tag_type(field_t2_pointer.subtype());
+        to_struct_tag_type(field_t2_pointer.base_type());
       const struct_typet &subtype_struct = to_struct_type(
         new_symbol_table.lookup_ref(field_t2_subtype.get_identifier()).type);
       REQUIRE(is_valid_java_array(subtype_struct));
@@ -91,7 +91,7 @@ SCENARIO(
           field_t3.type(), JAVA_REFERENCE_ARRAY_CLASSID);
 
       const struct_tag_typet &field_t3_subtype =
-        to_struct_tag_type(field_t3_pointer.subtype());
+        to_struct_tag_type(field_t3_pointer.base_type());
       const struct_typet &subtype_struct = to_struct_type(
         new_symbol_table.lookup_ref(field_t3_subtype.get_identifier()).type);
       REQUIRE(is_valid_java_array(subtype_struct));
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
index 81bf5374810..5bb1168653d 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp
@@ -56,7 +56,7 @@ SCENARIO(
         require_type::require_pointer_to_tag(field.type(), inner_class_prefix);
       java_generic_struct_tag_typet inner_class_tag =
         require_type::require_java_generic_struct_tag_type(
-          field_type.subtype(),
+          field_type.base_type(),
           inner_class_prefix,
           {
             {require_type::type_argument_kindt::Var,
@@ -79,7 +79,7 @@ SCENARIO(
           shadowing_field.type(), shadowing_inner_class_prefix);
         java_generic_struct_tag_typet shadowing_inner_class_tag =
           require_type::require_java_generic_struct_tag_type(
-            shadowing_field_type.subtype(),
+            shadowing_field_type.base_type(),
             shadowing_inner_class_prefix,
             {
               {require_type::type_argument_kindt::Var,
diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
index 95868de6d27..10436984657 100644
--- a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
+++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_annotations.cpp
@@ -53,10 +53,9 @@ static void require_matching_annotations(
     annotations.begin(),
     annotations.end(),
     std::back_inserter(annotation_names),
-    [](const java_bytecode_parse_treet::annotationt &annotation)
-    {
+    [](const java_bytecode_parse_treet::annotationt &annotation) {
       return get_base_name(
-        require_type::require_pointer(annotation.type, {}).subtype());
+        require_type::require_pointer(annotation.type, {}).base_type());
     });
   std::sort(annotation_names.begin(), annotation_names.end());
   std::sort(expected_annotations.begin(), expected_annotations.end());
diff --git a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp
index bc60ae59ab0..3c7b3d306b3 100644
--- a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp
+++ b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp
@@ -133,7 +133,7 @@ SCENARIO(
     {
       REQUIRE(
         make_query(block)[3].as<code_assignt>()[1].get().type() ==
-        test_class_type.subtype());
+        test_class_type.base_type());
     }
     THEN("The instruction assigns the field to 42")
     {
@@ -236,7 +236,7 @@ SCENARIO(
     {
       REQUIRE(
         make_query(block)[4].as<code_assignt>()[0].get().type() ==
-        test_class_type.subtype());
+        test_class_type.base_type());
     }
     THEN("The instruction allocates the array field, with a size of exactly 1")
     {
@@ -370,7 +370,7 @@ SCENARIO(
     {
       REQUIRE(
         make_query(block)[5].as<code_assignt>()[0].get().type() ==
-        test_class_type.subtype());
+        test_class_type.base_type());
     }
     THEN("The instruction makes the length nondet")
     {
diff --git a/src/analyses/goto_check_c.cpp b/src/analyses/goto_check_c.cpp
index d4249931f99..dff22d10b3d 100644
--- a/src/analyses/goto_check_c.cpp
+++ b/src/analyses/goto_check_c.cpp
@@ -1732,7 +1732,7 @@ bool goto_check_ct::check_rec_member(
   if(member_offset_opt.has_value())
   {
     pointer_typet new_pointer_type = to_pointer_type(deref.pointer().type());
-    new_pointer_type.subtype() = member.type();
+    new_pointer_type.base_type() = member.type();
 
     const exprt char_pointer = typecast_exprt::conditional_cast(
       deref.pointer(), pointer_type(char_type()));
diff --git a/src/analyses/variable-sensitivity/two_value_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/two_value_pointer_abstract_object.cpp
index f76526f0ac4..532c9d95ed8 100644
--- a/src/analyses/variable-sensitivity/two_value_pointer_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/two_value_pointer_abstract_object.cpp
@@ -38,7 +38,7 @@ abstract_object_pointert two_value_pointer_abstract_objectt::read_dereference(
   const namespacet &ns) const
 {
   pointer_typet pointer_type(to_pointer_type(type()));
-  const typet &pointed_to_type = pointer_type.subtype();
+  const typet &pointed_to_type = pointer_type.base_type();
 
   return env.abstract_object_factory(pointed_to_type, ns, true, false);
 }
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 5f7bf099c30..a1cb4dbe890 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -50,9 +50,9 @@ void symbol_factoryt::gen_nondet_init(
   {
     // dereferenced type
     const pointer_typet &pointer_type=to_pointer_type(type);
-    const typet &subtype = pointer_type.subtype();
+    const typet &base_type = pointer_type.base_type();
 
-    if(subtype.id() == ID_code)
+    if(base_type.id() == ID_code)
     {
       // Handle the pointer-to-code case separately:
       // leave as nondet_ptr to allow `remove_function_pointers`
@@ -62,9 +62,10 @@ void symbol_factoryt::gen_nondet_init(
       return;
     }
 
-    if(subtype.id() == ID_struct_tag)
+    if(base_type.id() == ID_struct_tag)
     {
-      const irep_idt struct_tag = to_struct_tag_type(subtype).get_identifier();
+      const irep_idt struct_tag =
+        to_struct_tag_type(base_type).get_identifier();
 
       if(
         recursion_set.find(struct_tag) != recursion_set.end() &&
@@ -79,7 +80,7 @@ void symbol_factoryt::gen_nondet_init(
 
     code_blockt non_null_inst;
 
-    typet object_type = subtype;
+    typet object_type = base_type;
     if(object_type.id() == ID_empty)
       object_type = char_type();
 
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 455b83ccc49..5b365bb6891 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2665,7 +2665,7 @@ exprt c_typecheck_baset::do_special_functions(
     else
     {
       // Won't do void *
-      const auto &subtype = to_pointer_type(pointer_expr.type()).subtype();
+      const auto &subtype = to_pointer_type(pointer_expr.type()).base_type();
       if(subtype.id() == ID_empty)
       {
         error().source_location = f_op.source_location();
diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
index 5fc5413601d..4d2dd3a49bc 100644
--- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
+++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
@@ -914,7 +914,7 @@ static void instantiate_sync_lock_release(
   // This built-in function releases the lock acquired by
   // __sync_lock_test_and_set. Normally this means writing the constant 0 to
   // *ptr.
-  const typet &type = to_pointer_type(parameter_exprs[0].type()).subtype();
+  const typet &type = to_pointer_type(parameter_exprs[0].type()).base_type();
 
   // place operations on *ptr in an atomic section
   block.add(code_expressiont{side_effect_expr_function_callt{
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index d4b0db4fcd3..f9f11733525 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -899,7 +899,7 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
           pointer_typet ptr_sub=pointer_type(type);
           c_qualifierst qual_from;
           qual_from.read(expr.type());
-          qual_from.write(ptr_sub.subtype());
+          qual_from.write(ptr_sub.base_type());
           make_ptr_typecast(address, ptr_sub);
 
           const dereference_exprt deref(address);
diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp
index e0f0e8de43e..85409731cbe 100644
--- a/src/cpp/cpp_typecheck_virtual_table.cpp
+++ b/src/cpp/cpp_typecheck_virtual_table.cpp
@@ -37,7 +37,7 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
       to_pointer_type(code_type.parameters()[0].type());
 
     const irep_idt &class_id =
-      parameter_pointer_type.subtype().get(ID_identifier);
+      parameter_pointer_type.base_type().get(ID_identifier);
 
     std::map<irep_idt, exprt> &value_map =
       vt_value_maps[class_id];
diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp
index 1d69c96a393..c32114ae357 100644
--- a/src/goto-harness/function_call_harness_generator.cpp
+++ b/src/goto-harness/function_call_harness_generator.cpp
@@ -400,7 +400,7 @@ void function_call_harness_generatort::validate_options(
     }
 
     if(!can_cast_type<code_typet>(
-         to_pointer_type(function_pointer_type).subtype()))
+         to_pointer_type(function_pointer_type).base_type()))
     {
       throw invalid_command_line_argument_exceptiont{
         "`" + id2string(nullable) + "' is not pointing to a function",
diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp
index ce16ab6c6cf..1a79b787da4 100644
--- a/src/goto-harness/recursive_initialization.cpp
+++ b/src/goto-harness/recursive_initialization.cpp
@@ -980,10 +980,10 @@ code_blockt recursive_initializationt::build_function_pointer_constructor(
 {
   PRECONDITION(can_cast_type<pointer_typet>(result.type()));
   const auto &result_type = to_pointer_type(result.type());
-  PRECONDITION(can_cast_type<pointer_typet>(result_type.subtype()));
-  const auto &function_pointer_type = to_pointer_type(result_type.subtype());
-  PRECONDITION(can_cast_type<code_typet>(function_pointer_type.subtype()));
-  const auto &function_type = to_code_type(function_pointer_type.subtype());
+  PRECONDITION(can_cast_type<pointer_typet>(result_type.base_type()));
+  const auto &function_pointer_type = to_pointer_type(result_type.base_type());
+  PRECONDITION(can_cast_type<code_typet>(function_pointer_type.base_type()));
+  const auto &function_type = to_code_type(function_pointer_type.base_type());
 
   std::vector<exprt> targets;
 
diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp
index 981c011e8af..8b3debe3c5f 100644
--- a/src/goto-instrument/thread_instrumentation.cpp
+++ b/src/goto-instrument/thread_instrumentation.cpp
@@ -134,6 +134,6 @@ void mutex_init_instrumentation(goto_modelt &goto_model)
     mutex_init_instrumentation(
       goto_model.symbol_table,
       gf_entry.second.body,
-      to_pointer_type(lock_type).subtype());
+      to_pointer_type(lock_type).base_type());
   }
 }
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 699b1dc14eb..2f4ad8868ae 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1207,7 +1207,7 @@ void goto_convertt::do_function_call_symbol(
       exprt list_arg_cast = list_arg;
       if(
         list_arg.type().id() == ID_pointer &&
-        to_pointer_type(list_arg.type()).subtype().id() == ID_empty)
+        to_pointer_type(list_arg.type()).base_type().id() == ID_empty)
       {
         list_arg_cast =
           typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))};
@@ -1272,7 +1272,7 @@ void goto_convertt::do_function_call_symbol(
 
     if(
       dest_expr.type().id() == ID_pointer &&
-      to_pointer_type(dest_expr.type()).subtype().id() == ID_empty)
+      to_pointer_type(dest_expr.type()).base_type().id() == ID_empty)
     {
       dest_expr =
         typecast_exprt{dest_expr, pointer_type(pointer_type(empty_typet{}))};
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index 8ed67d19b53..9d8738d407e 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -655,7 +655,7 @@ void goto_convertt::remove_overflow(
   optionalt<typet> result_type;
   if(result.type().id() == ID_pointer)
   {
-    result_type = to_pointer_type(result.type()).subtype();
+    result_type = to_pointer_type(result.type()).base_type();
     code_assignt result_assignment{dereference_exprt{result},
                                    typecast_exprt{operation, *result_type},
                                    expr.source_location()};
diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp
index b476c7b6b20..795e42972b4 100644
--- a/src/goto-programs/json_expr.cpp
+++ b/src/goto-programs/json_expr.cpp
@@ -144,7 +144,7 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
   else if(type.id() == ID_pointer)
   {
     result["name"] = json_stringt("pointer");
-    result["subtype"] = json(to_pointer_type(type).subtype(), ns, mode);
+    result["subtype"] = json(to_pointer_type(type).base_type(), ns, mode);
   }
   else if(type.id() == ID_bool)
   {
diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp
index b51266f406e..dceecb4fbff 100644
--- a/src/goto-programs/restrict_function_pointers.cpp
+++ b/src/goto-programs/restrict_function_pointers.cpp
@@ -126,7 +126,7 @@ void function_pointer_restrictionst::typecheck_function_pointer_restrictions(
                                            id2string(restriction.first)};
     }
     auto const &function_type =
-      to_pointer_type(function_pointer_type).subtype();
+      to_pointer_type(function_pointer_type).base_type();
     if(function_type.id() != ID_code)
     {
       throw invalid_restriction_exceptiont{"not a function pointer: " +
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
index 3f9be37d7c5..df33dde42af 100644
--- a/src/goto-programs/xml_expr.cpp
+++ b/src/goto-programs/xml_expr.cpp
@@ -66,7 +66,7 @@ xmlt xml(const typet &type, const namespacet &ns)
   {
     result.name = "pointer";
     result.new_element("subtype").new_element() =
-      xml(to_pointer_type(type).subtype(), ns);
+      xml(to_pointer_type(type).base_type(), ns);
   }
   else if(type.id() == ID_bool)
   {
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
index 745746e0500..66efc026a74 100644
--- a/src/goto-symex/auto_objects.cpp
+++ b/src/goto-symex/auto_objects.cpp
@@ -53,17 +53,16 @@ void goto_symext::initialize_auto_object(const exprt &expr, statet &state)
   else if(type.id()==ID_pointer)
   {
     const pointer_typet &pointer_type=to_pointer_type(type);
-    const typet &subtype = pointer_type.subtype();
+    const typet &base_type = pointer_type.base_type();
 
     // we don't like function pointers and
     // we don't like void *
-    if(subtype.id()!=ID_code &&
-       subtype.id()!=ID_empty)
+    if(base_type.id() != ID_code && base_type.id() != ID_empty)
     {
       // could be NULL nondeterministically
 
       address_of_exprt address_of_expr(
-        make_auto_object(pointer_type.subtype(), state), pointer_type);
+        make_auto_object(base_type, state), pointer_type);
 
       if_exprt rhs(
         side_effect_expr_nondett(bool_typet(), expr.source_location()),
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index 979398c9193..6cf1e09efd2 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -389,7 +389,7 @@ void goto_symext::constant_propagate_empty_string(
 {
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const constant_exprt length = from_integer(0, length_type);
 
@@ -417,7 +417,7 @@ bool goto_symext::constant_propagate_string_concat(
 {
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const refined_string_exprt &s1 = to_string_expr(f_l1.arguments().at(2));
   const auto s1_data_opt = try_evaluate_constant_string(state, s1.content());
@@ -472,7 +472,7 @@ bool goto_symext::constant_propagate_string_substring(
 
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
   const auto s_data_opt = try_evaluate_constant_string(state, s.content());
@@ -564,7 +564,7 @@ bool goto_symext::constant_propagate_integer_to_string(
 
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const auto &integer_opt =
     try_evaluate_constant(state, f_l1.arguments().at(2));
@@ -640,7 +640,7 @@ bool goto_symext::constant_propagate_delete_char_at(
 
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
   const auto s_data_opt = try_evaluate_constant_string(state, s.content());
@@ -714,7 +714,7 @@ bool goto_symext::constant_propagate_delete(
 
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
   const auto s_data_opt = try_evaluate_constant_string(state, s.content());
@@ -807,7 +807,7 @@ bool goto_symext::constant_propagate_set_length(
 
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const auto &new_length_opt =
     try_evaluate_constant(state, f_l1.arguments().at(3));
@@ -889,7 +889,7 @@ bool goto_symext::constant_propagate_set_char_at(
 
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
   const auto s_data_opt = try_evaluate_constant_string(state, s.content());
@@ -952,7 +952,7 @@ bool goto_symext::constant_propagate_case_change(
 {
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
   const auto s_data_opt = try_evaluate_constant_string(state, s.content());
@@ -1013,7 +1013,7 @@ bool goto_symext::constant_propagate_replace(
 {
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
   const auto s_data_opt = try_evaluate_constant_string(state, s.content());
@@ -1121,7 +1121,7 @@ bool goto_symext::constant_propagate_trim(
 {
   const auto &f_type = f_l1.function_type();
   const auto &length_type = f_type.domain().at(0);
-  const auto &char_type = to_pointer_type(f_type.domain().at(1)).subtype();
+  const auto &char_type = to_pointer_type(f_type.domain().at(1)).base_type();
 
   const refined_string_exprt &s = to_string_expr(f_l1.arguments().at(2));
   const auto s_data_opt = try_evaluate_constant_string(state, s.content());
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index e669329a4fd..c6913794efc 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -244,7 +244,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
   {
     auto &address_of_expr = to_address_of_expr(expr);
     rename_address<level>(address_of_expr.object(), ns);
-    to_pointer_type(expr.type()).subtype() =
+    to_pointer_type(expr.type()).base_type() =
       as_const(address_of_expr).object().type();
     return renamedt<exprt, level>{std::move(expr)};
   }
@@ -660,7 +660,7 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
   }
   else if(type.id() == ID_pointer)
   {
-    return requires_renaming(to_pointer_type(type).subtype(), ns);
+    return requires_renaming(to_pointer_type(type).base_type(), ns);
   }
   else if(type.id() == ID_union_tag)
   {
@@ -742,7 +742,7 @@ void goto_symex_statet::rename(
   }
   else if(type.id()==ID_pointer)
   {
-    rename<level>(to_pointer_type(type).subtype(), irep_idt(), ns);
+    rename<level>(to_pointer_type(type).base_type(), irep_idt(), ns);
   }
 
   if(level==L2 &&
diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp
index e2179e473ee..bd3c2801366 100644
--- a/src/goto-symex/renaming_level.cpp
+++ b/src/goto-symex/renaming_level.cpp
@@ -188,8 +188,8 @@ typet get_original_name(typet type)
   }
   else if(type.id() == ID_pointer)
   {
-    type.subtype() =
-      get_original_name(std::move(to_pointer_type(type).subtype()));
+    to_pointer_type(type).base_type() =
+      get_original_name(std::move(to_pointer_type(type).base_type()));
   }
   return type;
 }
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index a0a16ffc1a2..9d1cee75cad 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -67,9 +67,9 @@ void goto_symext::symex_allocate(
   // is the type given?
   if(
     code.type().id() == ID_pointer &&
-    to_pointer_type(code.type()).subtype().id() != ID_empty)
+    to_pointer_type(code.type()).base_type().id() != ID_empty)
   {
-    object_type = to_pointer_type(code.type()).subtype();
+    object_type = to_pointer_type(code.type()).base_type();
   }
   else
   {
@@ -223,7 +223,7 @@ static exprt va_list_entry(
 
   // Visual Studio has va_list == char* and stores parameters of size no
   // greater than the size of a pointer as immediate values
-  if(lhs_type.subtype().id() != ID_pointer)
+  if(lhs_type.base_type().id() != ID_pointer)
   {
     auto parameter_size = size_of_expr(parameter_expr.type(), ns);
     CHECK_RETURN(parameter_size.has_value());
@@ -503,10 +503,10 @@ void goto_symext::symex_cpp_new(
   {
     exprt size_arg =
       clean_expr(static_cast<const exprt &>(code.find(ID_size)), state, false);
-    symbol.type = array_typet(pointer_type.subtype(), size_arg);
+    symbol.type = array_typet(pointer_type.base_type(), size_arg);
   }
   else
-    symbol.type = pointer_type.subtype();
+    symbol.type = pointer_type.base_type();
 
   symbol.type.set(ID_C_dynamic, true);
 
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index f98944d178a..7a045bb196a 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -389,9 +389,7 @@ void goto_symext::dereference_rec(
     exprt &object=address_of_expr.object();
 
     expr = address_arithmetic(
-      object,
-      state,
-      to_pointer_type(expr.type()).subtype().id() == ID_array);
+      object, state, to_pointer_type(expr.type()).base_type().id() == ID_array);
   }
   else if(expr.id()==ID_typecast)
   {
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 0c083ee0627..ef8b584daed 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -518,7 +518,7 @@ void value_sett::get_value_set_rec(
       // we'll add null, in case it's not there yet
       insert(
         dest,
-        exprt(ID_null_object, to_pointer_type(expr_type).subtype()),
+        exprt(ID_null_object, to_pointer_type(expr_type).base_type()),
         offsett());
     }
     else
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index b716837fe01..2a433b9bf00 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -447,7 +447,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 {
   const pointer_typet &pointer_type =
     type_checked_cast<pointer_typet>(pointer_expr.type());
-  const typet &dereference_type = pointer_type.subtype();
+  const typet &dereference_type = pointer_type.base_type();
 
   if(what.id()==ID_unknown ||
      what.id()==ID_invalid)
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index de109fe5767..74757b41c9e 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -613,9 +613,9 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
       // Support for void* is a gcc extension, with the size treated as 1 byte
       // (no division required below).
       // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
-      if(lhs_pt.subtype().id() != ID_empty)
+      if(lhs_pt.base_type().id() != ID_empty)
       {
-        auto element_size_opt = pointer_offset_size(lhs_pt.subtype(), ns);
+        auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
         CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
 
         if(*element_size_opt != 1)
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index 91f59a7c0ab..4dfaa2fc34e 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -94,7 +94,7 @@ exprt pointer_logict::pointer_expr(
 
   const exprt &object_expr=objects[pointer.object];
 
-  typet subtype = type.subtype();
+  typet subtype = type.base_type();
   // This is a gcc extension.
   // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
   if(subtype.id() == ID_empty)
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
index 9a71f2937b5..e7f883a7066 100644
--- a/src/util/base_type.cpp
+++ b/src/util/base_type.cpp
@@ -83,26 +83,26 @@ void base_type_rec(
   }
   else if(type.id()==ID_pointer)
   {
-    typet &subtype=to_pointer_type(type).subtype();
+    typet &base_type = to_pointer_type(type).base_type();
 
     // we need to avoid running into an infinite loop
     if(
-      subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag ||
-      subtype.id() == ID_union_tag)
+      base_type.id() == ID_c_enum_tag || base_type.id() == ID_struct_tag ||
+      base_type.id() == ID_union_tag)
     {
-      const irep_idt &id = to_tag_type(subtype).get_identifier();
+      const irep_idt &id = to_tag_type(base_type).get_identifier();
 
       if(symb.find(id)!=symb.end())
         return;
 
       symb.insert(id);
 
-      base_type_rec(subtype, ns, symb);
+      base_type_rec(base_type, ns, symb);
 
       symb.erase(id);
     }
     else
-      base_type_rec(subtype, ns, symb);
+      base_type_rec(base_type, ns, symb);
   }
 }
 
@@ -228,7 +228,7 @@ bool base_type_eqt::base_type_eq_rec(
   else if(type1.id()==ID_pointer)
   {
     return base_type_eq_rec(
-      to_pointer_type(type1).subtype(), to_pointer_type(type2).subtype());
+      to_pointer_type(type1).base_type(), to_pointer_type(type2).base_type());
   }
   else if(type1.id()==ID_array)
   {
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index dd6aa815bf2..9696b0c4749 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -193,7 +193,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
       const auto &unary_expr = to_unary_expr(src);
       const auto &pointer_type = to_pointer_type(src.type());
       return os << "pointer(" << format(unary_expr.op()) << ", "
-                << format(pointer_type.subtype()) << ')';
+                << format(pointer_type.base_type()) << ')';
     }
     else
     {
@@ -201,7 +201,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
       const auto width = pointer_type.get_width();
       auto int_value = bvrep2integer(src.get_value(), width, false);
       return os << "pointer(0x" << integer2string(int_value, 16) << ", "
-                << format(pointer_type.subtype()) << ')';
+                << format(pointer_type.base_type()) << ')';
     }
   }
   else
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
index 71140a518cf..cca40c5b201 100644
--- a/src/util/format_type.cpp
+++ b/src/util/format_type.cpp
@@ -63,7 +63,7 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
   const auto &id = type.id();
 
   if(id == ID_pointer)
-    return os << format(to_pointer_type(type).subtype()) << '*';
+    return os << format(to_pointer_type(type).base_type()) << '*';
   else if(id == ID_array)
   {
     const auto &t = to_array_type(type);
diff --git a/src/util/pointer_expr.cpp b/src/util/pointer_expr.cpp
index dcc6f319747..caac303e911 100644
--- a/src/util/pointer_expr.cpp
+++ b/src/util/pointer_expr.cpp
@@ -129,21 +129,21 @@ object_address_exprt::object_address_exprt(const symbol_exprt &object)
 
 symbol_exprt object_address_exprt::object_expr() const
 {
-  return symbol_exprt(object_identifier(), to_pointer_type(type()).subtype());
+  return symbol_exprt(object_identifier(), to_pointer_type(type()).base_type());
 }
 
 field_address_exprt::field_address_exprt(
-  exprt base,
+  exprt compound_ptr,
   const irep_idt &component_name,
   pointer_typet _type)
-  : unary_exprt(ID_field_address, std::move(base), std::move(_type))
+  : unary_exprt(ID_field_address, std::move(compound_ptr), std::move(_type))
 {
-  const auto &base_type = base.type();
-  PRECONDITION(base_type.id() == ID_pointer);
-  const auto &base_sub_type = base_type.subtype();
+  const auto &compound_ptr_type = compound_ptr.type();
+  PRECONDITION(compound_ptr_type.id() == ID_pointer);
+  const auto &compound_type = to_pointer_type(compound_ptr_type).base_type();
   PRECONDITION(
-    base_sub_type.id() == ID_struct || base_sub_type.id() == ID_struct_tag ||
-    base_sub_type.id() == ID_union || base_sub_type.id() == ID_union_tag);
+    compound_type.id() == ID_struct || compound_type.id() == ID_struct_tag ||
+    compound_type.id() == ID_union || compound_type.id() == ID_union_tag);
   set(ID_component_name, component_name);
 }
 
@@ -153,7 +153,7 @@ element_address_exprt::element_address_exprt(exprt base, exprt index)
       ID_element_address,
       std::move(index),
       pointer_typet(
-        to_array_type(base.type()).subtype(),
+        to_array_type(base.type()).element_type(),
         to_pointer_type(base.type()).get_width()))
 {
 }
@@ -176,7 +176,7 @@ const exprt &object_descriptor_exprt::root_object(const exprt &expr)
 }
 
 /// Check that the dereference expression has the right number of operands,
-/// refers to something with a pointer type, and that its type is the subtype
+/// refers to something with a pointer type, and that its type is the base type
 /// of that pointer type. Throws or raises an invariant if not, according to
 /// validation mode.
 /// \param expr: expression to validate
@@ -203,7 +203,7 @@ void dereference_exprt::validate(
 
   DATA_CHECK(
     vm,
-    dereference_expr.type() == pointer_type->subtype(),
-    "dereference expression's type must match the subtype of the type of its "
+    dereference_expr.type() == pointer_type->base_type(),
+    "dereference expression's type must match the base type of the type of its "
     "operand");
 }
diff --git a/src/util/pointer_expr.h b/src/util/pointer_expr.h
index 4d2c6c4fa79..1336647671e 100644
--- a/src/util/pointer_expr.h
+++ b/src/util/pointer_expr.h
@@ -23,10 +23,26 @@ class namespacet;
 class pointer_typet : public bitvector_typet
 {
 public:
-  pointer_typet(typet _subtype, std::size_t width)
+  pointer_typet(typet _base_type, std::size_t width)
     : bitvector_typet(ID_pointer, width)
   {
-    subtype().swap(_subtype);
+    subtype().swap(_base_type);
+  }
+
+  /// The type of the data what we point to.
+  /// This method is preferred over .subtype(),
+  /// which will eventually be deprecated.
+  const typet &base_type() const
+  {
+    return subtype();
+  }
+
+  /// The type of the data what we point to.
+  /// This method is preferred over .subtype(),
+  /// which will eventually be deprecated.
+  typet &base_type()
+  {
+    return subtype();
   }
 
   signedbv_typet difference_type() const
@@ -78,7 +94,8 @@ inline pointer_typet &to_pointer_type(typet &type)
 /// if the given typet is a pointer of type void.
 inline bool is_void_pointer(const typet &type)
 {
-  return type.id() == ID_pointer && type.subtype().id() == ID_empty;
+  return type.id() == ID_pointer &&
+         to_pointer_type(type).base_type().id() == ID_empty;
 }
 
 /// The reference type
@@ -416,7 +433,7 @@ class object_address_exprt : public nullary_exprt
   /// returns the type of the object whose address is represented
   const typet &object_type() const
   {
-    return type().subtype();
+    return type().base_type();
   }
 
   symbol_exprt object_expr() const;
@@ -492,12 +509,12 @@ class field_address_exprt : public unary_exprt
   /// returns the type of the field whose address is represented
   const typet &field_type() const
   {
-    return type().subtype();
+    return type().base_type();
   }
 
   const typet &compound_type() const
   {
-    return to_pointer_type(base().type()).subtype();
+    return to_pointer_type(base().type()).base_type();
   }
 
   const irep_idt &component_name() const
@@ -564,7 +581,7 @@ class element_address_exprt : public binary_exprt
   /// returns the type of the array element whose address is represented
   const typet &element_type() const
   {
-    return type().subtype();
+    return type().base_type();
   }
 
   exprt &base()
@@ -627,10 +644,10 @@ inline element_address_exprt &to_element_address_expr(exprt &expr)
 class dereference_exprt : public unary_exprt
 {
 public:
+  // The given operand must have pointer type.
   explicit dereference_exprt(const exprt &op)
-    : unary_exprt(ID_dereference, op, op.type().subtype())
+    : unary_exprt(ID_dereference, op, to_pointer_type(op.type()).base_type())
   {
-    PRECONDITION(op.type().id() == ID_pointer);
   }
 
   dereference_exprt(exprt op, typet type)
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
index 4c0eb969b29..caca616f654 100644
--- a/src/util/pointer_predicates.cpp
+++ b/src/util/pointer_predicates.cpp
@@ -73,7 +73,7 @@ exprt good_pointer_def(
   const namespacet &ns)
 {
   const pointer_typet &pointer_type = to_pointer_type(pointer.type());
-  const typet &dereference_type=pointer_type.subtype();
+  const typet &dereference_type = pointer_type.base_type();
 
   const auto size_of_expr_opt = size_of_expr(dereference_type, ns);
   CHECK_RETURN(size_of_expr_opt.has_value());
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index e4fc2508780..9afb82cc23d 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -881,7 +881,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
          to_constant_expr(op_plus_expr.op0()).get_value() == ID_NULL)))
     {
       auto sub_size =
-        pointer_offset_size(to_pointer_type(op_type).subtype(), ns);
+        pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
       if(sub_size.has_value())
       {
         auto new_expr = expr;
@@ -956,7 +956,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     (expr_type.id() == ID_signedbv || expr_type.id() == ID_unsignedbv) &&
     op_type.id() == ID_pointer && expr.op().id() == ID_plus)
   {
-    const auto step = pointer_offset_size(to_pointer_type(op_type).subtype(), ns);
+    const auto step =
+      pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
 
     if(step.has_value() && *step != 0)
     {
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 87b566759d8..fb8c384773b 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -95,7 +95,7 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
         {
           pointer_typet pointer_type = to_pointer_type(
             to_dereference_expr(new_index_expr.array()).pointer().type());
-          pointer_type.subtype() = new_index_expr.type();
+          pointer_type.base_type() = new_index_expr.type();
 
           typecast_exprt typecast_expr(
             from_integer((*step_size) * (*index) + address, index_type()),
@@ -140,7 +140,7 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
         {
           pointer_typet pointer_type = to_pointer_type(
             to_dereference_expr(new_member_expr.struct_op()).pointer().type());
-          pointer_type.subtype() = new_member_expr.type();
+          pointer_type.base_type() = new_member_expr.type();
           typecast_exprt typecast_expr(
             from_integer(address + *offset, index_type()), pointer_type);
           return dereference_exprt{typecast_expr};