diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index 024eaeec24c..88d7ca8fba7 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -735,13 +735,23 @@ class java_generic_parametert : public reference_typet
   }
 };
 
+/// Check whether a reference to a typet is a java generic parameter/variable,
+/// e.g., `T` in `List<T>`.
+/// \param type: Source type.
+/// \return True if \p type is a generic Java parameter type
+template <>
+inline bool can_cast_type<java_generic_parametert>(const typet &base)
+{
+  return is_reference(base) && is_java_generic_parameter_tag(base.subtype());
+}
+
 /// Checks whether the type is a java generic parameter/variable, e.g., `T` in
 /// `List<T>`.
 /// \param type: the type to check
 /// \return true if type is a generic Java parameter type
 inline bool is_java_generic_parameter(const typet &type)
 {
-  return is_reference(type) && is_java_generic_parameter_tag(type.subtype());
+  return can_cast_type<java_generic_parametert>(type);
 }
 
 /// \param type: source type
diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 2691b12b41b..bb9a21128cb 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -21,93 +21,11 @@ pointer_typet select_pointer_typet::convert_pointer_type(
   const namespacet &ns) const
 {
   (void)ns; // unused parameter
-  // if we have a map of generic parameters -> types and the pointer is
-  // a generic parameter, specialize it with concrete types
-  if(!generic_parameter_specialization_map.empty())
-  {
-    generic_parameter_recursion_trackingt visited;
-    const auto &type = specialize_generics(
-      pointer_type, generic_parameter_specialization_map, visited);
-    INVARIANT(visited.empty(), "recursion stack must be empty here");
-    return type;
-  }
-  else
-  {
-    return pointer_type;
-  }
+  return specialize_generics(
+    pointer_type, generic_parameter_specialization_map);
 }
 
-pointer_typet select_pointer_typet::specialize_generics(
-  const pointer_typet &pointer_type,
-  const generic_parameter_specialization_mapt
-    &generic_parameter_specialization_map,
-  generic_parameter_recursion_trackingt &visited_nodes) const
-{
-  if(is_java_generic_parameter(pointer_type))
-  {
-    const java_generic_parametert &parameter =
-      to_java_generic_parameter(pointer_type);
-    const irep_idt &parameter_name = parameter.get_name();
-
-    // avoid infinite recursion by looking at each generic argument from
-    // previous assignments
-    if(visited_nodes.find(parameter_name) != visited_nodes.end())
-    {
-      const optionalt<pointer_typet> result = get_recursively_instantiated_type(
-        parameter_name, generic_parameter_specialization_map);
-      return result.has_value() ? result.value() : pointer_type;
-    }
-
-    if(generic_parameter_specialization_map.count(parameter_name) == 0)
-    {
-      // this means that the generic pointer_type has not been specialized
-      // in the current context (e.g., the method under test is generic);
-      // we return the pointer_type itself which is basically a pointer to
-      // its upper bound
-      return pointer_type;
-    }
-    const pointer_typet &type =
-      generic_parameter_specialization_map.find(parameter_name)->second.back();
-
-    // generic parameters can be adopted from outer classes or superclasses so
-    // we may need to search for the concrete type recursively
-    if(!is_java_generic_parameter(type))
-      return type;
-
-    visited_nodes.insert(parameter_name);
-    const auto returned_type = specialize_generics(
-      to_java_generic_parameter(type),
-      generic_parameter_specialization_map,
-      visited_nodes);
-    visited_nodes.erase(parameter_name);
-    return returned_type;
-  }
-  else if(pointer_type.subtype().id() == ID_struct_tag)
-  {
-    // if the pointer is an array, recursively specialize its element type
-    const auto &array_subtype = to_struct_tag_type(pointer_type.subtype());
-    if(is_java_array_tag(array_subtype.get_identifier()))
-    {
-      const typet &array_element_type = java_array_element_type(array_subtype);
-      if(array_element_type.id() == ID_pointer)
-      {
-        const pointer_typet &new_array_type = specialize_generics(
-          to_pointer_type(array_element_type),
-          generic_parameter_specialization_map,
-          visited_nodes);
-
-        pointer_typet replacement_array_type = java_array_type('a');
-        replacement_array_type.subtype().set(ID_element_type, new_array_type);
-        return replacement_array_type;
-      }
-    }
-  }
-  return pointer_type;
-}
-
-/// Return the first concrete type instantiation if any such exists. This method
-/// is only to be called when \ref select_pointer_typet::specialize_generics
-/// cannot find an instantiation due to a loop in its recursion.
+/// Return the first concrete type instantiation if any such exists.
 ///
 /// Example:
 /// `class MyGeneric<T,U> { MyGeneric<U,T> gen; T t;}`
@@ -118,94 +36,62 @@ pointer_typet select_pointer_typet::specialize_generics(
 ///
 /// Note that the top of the stacks for T and U create a recursion T -> U,
 /// U-> T. We want to break it and specialize `T my.gen.t` to `String my.gen.t`.
-/// \param parameter_name: The name of the generic parameter type we want to
-///   have instantiated
+/// \param pointer_type: The pointer type to specialize
 /// \param generic_parameter_specialization_map: Map of type names to
 ///   specialization stack
 /// \return The first instantiated type for the generic type or nothing if no
 ///   such instantiation exists.
-optionalt<pointer_typet>
-select_pointer_typet::get_recursively_instantiated_type(
-  const irep_idt &parameter_name,
+pointer_typet select_pointer_typet::specialize_generics(
+  const pointer_typet &pointer_type,
   const generic_parameter_specialization_mapt
     &generic_parameter_specialization_map) const
 {
-  generic_parameter_recursion_trackingt visited;
-  const size_t max_depth =
-    generic_parameter_specialization_map.find(parameter_name)->second.size();
-
-  irep_idt current_parameter = parameter_name;
-  for(size_t depth = 0; depth < max_depth; depth++)
+  auto parameter = type_try_dynamic_cast<java_generic_parametert>(pointer_type);
+  if(parameter != nullptr)
   {
-    const auto retval = get_recursively_instantiated_type(
-      current_parameter, generic_parameter_specialization_map, visited, depth);
-    if(retval.has_value())
+    irep_idt parameter_name = parameter->get_name();
+
+    generic_parameter_specialization_mapt spec_map_copy =
+      generic_parameter_specialization_map;
+    while(true)
     {
-      CHECK_RETURN(!is_java_generic_parameter(*retval));
-      return retval;
+      auto types_it = spec_map_copy.find(parameter_name);
+      if(types_it == spec_map_copy.end() || types_it->second.empty())
+      {
+        // This means that the generic pointer_type has not been specialized
+        // in the current context (e.g., the method under test is generic);
+        // we return the pointer_type itself which is a pointer to its upper
+        // bound
+        return pointer_type;
+      }
+      const reference_typet &type = types_it->second.back();
+      types_it->second.pop_back();
+      if(!is_java_generic_parameter(type))
+        return type;
+      parameter_name = to_java_generic_parameter(type).get_name();
     }
-    CHECK_RETURN(visited.empty());
-
-    const auto &entry =
-      generic_parameter_specialization_map.find(current_parameter)
-        ->second.back();
-    current_parameter = to_java_generic_parameter(entry).get_name();
   }
-  return {};
-}
 
-/// See get_recursively instantiated_type, the additional parameters just track
-/// the recursion to prevent visiting the same depth again and specify which
-/// stack depth is analyzed.
-/// \param parameter_name: The name of the generic parameter type we want to
-///   have instantiated
-/// \param generic_parameter_specialization_map: Map of type names to
-///   specialization stack
-/// \param visited: Tracks the visited parameter names
-/// \param depth: Stack depth to analyze
-/// \return if this type is not a generic type, it is returned as a valid
-///   instantiation, if nothing can be found at the given depth, en empty
-///   optional is returned
-optionalt<pointer_typet>
-select_pointer_typet::get_recursively_instantiated_type(
-  const irep_idt &parameter_name,
-  const generic_parameter_specialization_mapt
-    &generic_parameter_specialization_map,
-  generic_parameter_recursion_trackingt &visited,
-  const size_t depth) const
-{
-  const auto &val = generic_parameter_specialization_map.find(parameter_name);
-  INVARIANT(
-    val != generic_parameter_specialization_map.end(),
-    "generic parameter must be a key in map");
-
-  const auto &replacements = val->second;
-
-  INVARIANT(
-    depth < replacements.size(), "cannot access elements outside stack");
-
-  // Check if there is a recursion loop, if yes return with nothing found
-  if(visited.find(parameter_name) != visited.end())
+  auto subtype =
+    type_try_dynamic_cast<struct_tag_typet>(pointer_type.subtype());
+  if(subtype != nullptr && is_java_array_tag(subtype->get_identifier()))
   {
-    return {};
-  }
+    // if the pointer is an array, recursively specialize its element type
+    auto array_element_type =
+      type_try_dynamic_cast<pointer_typet>(java_array_element_type(*subtype));
+    if(array_element_type == nullptr)
+      return pointer_type;
 
-  const size_t index = (replacements.size() - 1) - depth;
-  const auto &type = replacements[index];
+    const pointer_typet &new_array_type = specialize_generics(
+      *array_element_type,
+      generic_parameter_specialization_map);
 
-  if(!is_java_generic_parameter(type))
-  {
-    return type;
+    pointer_typet replacement_array_type = java_array_type('a');
+    replacement_array_type.subtype().set(ID_element_type, new_array_type);
+    return replacement_array_type;
   }
 
-  visited.insert(parameter_name);
-  const auto inst_val = get_recursively_instantiated_type(
-    to_java_generic_parameter(type).get_name(),
-    generic_parameter_specialization_map,
-    visited,
-    depth);
-  visited.erase(parameter_name);
-  return inst_val;
+  return pointer_type;
 }
 
 std::set<struct_tag_typet>
diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h
index bc4df621080..6e28029797f 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.h
+++ b/jbmc/src/java_bytecode/select_pointer_type.h
@@ -15,27 +15,44 @@ Author: Diffblue Ltd.
 
 #include <vector>
 
+#include "expr2java.h"
 #include "java_types.h"
 #include <util/optional.h>
 #include <util/std_types.h>
 
 typedef std::unordered_map<irep_idt, std::vector<reference_typet>>
   generic_parameter_specialization_mapt;
-typedef std::set<irep_idt> generic_parameter_recursion_trackingt;
+
+struct print_generic_parameter_specialization_map
+{
+  const generic_parameter_specialization_mapt &map;
+  const namespacet &ns;
+};
+
+template <typename ostream>
+ostream &
+operator<<(ostream &stm, const print_generic_parameter_specialization_map &map)
+{
+  stm << "Size: " << map.map.size() << "\n";
+  for(const auto &elt : map.map)
+  {
+    stm << elt.first << ": { ";
+    for(const auto &pointer_type : elt.second)
+    {
+      if(is_java_generic_parameter(pointer_type))
+        stm << to_java_generic_parameter(pointer_type).get_name() << "; ";
+      else
+        stm << type2java(pointer_type, map.ns) << "; ";
+    }
+    stm << "}\n";
+  }
+  return stm;
+}
 
 class namespacet;
 
 class select_pointer_typet
 {
-  optionalt<pointer_typet> get_recursively_instantiated_type(
-    const irep_idt &,
-    const generic_parameter_specialization_mapt &,
-    generic_parameter_recursion_trackingt &,
-    const size_t) const;
-  optionalt<pointer_typet> get_recursively_instantiated_type(
-    const irep_idt &parameter_name,
-    const generic_parameter_specialization_mapt &visited) const;
-
 public:
   virtual ~select_pointer_typet() = default;
 
@@ -88,8 +105,7 @@ class select_pointer_typet
   pointer_typet specialize_generics(
     const pointer_typet &pointer_type,
     const generic_parameter_specialization_mapt
-      &generic_parameter_specialization_map,
-    generic_parameter_recursion_trackingt &visited_nodes) const;
+      &generic_parameter_specialization_map) const;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H