diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index 22a335d1be6..9d5297ea7bc 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -123,6 +123,9 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     extra_entry_points.end(),
     std::back_inserter(extra_methods),
     build_load_method_by_regex);
+  const auto &new_points = build_extra_entry_points(cmd);
+  extra_methods.insert(
+    extra_methods.end(), new_points.begin(), new_points.end());
 
   if(cmd.isset("java-cp-include-files"))
   {
@@ -1207,3 +1210,13 @@ bool java_bytecode_languaget::to_expr(
 java_bytecode_languaget::~java_bytecode_languaget()
 {
 }
+
+/// This method should be overloaded to provide alternative approaches for
+/// specifying extra entry points. To provide a regex entry point, the command
+/// line option `--lazy-methods-extra-entry-point` can be used directly.
+std::vector<load_extra_methodst>
+java_bytecode_languaget::build_extra_entry_points(
+  const cmdlinet &command_line) const
+{
+  return {};
+}
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
index c754f59d8c6..c72a492f504 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.h
+++ b/jbmc/src/java_bytecode/java_bytecode_language.h
@@ -199,6 +199,8 @@ class java_bytecode_languaget:public languaget
   std::vector<irep_idt> java_load_classes;
 
 private:
+  virtual std::vector<load_extra_methodst>
+  build_extra_entry_points(const cmdlinet &command_line) const;
   const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
 
   /// Maps synthetic method names on to the particular type of synthetic method
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index 0ca7538e95a..2fdcde619b0 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -452,11 +452,17 @@ class java_generic_typet:public reference_typet
   }
 };
 
+template <>
+inline bool can_cast_type<java_generic_typet>(const typet &type)
+{
+  return is_reference(type) && type.get_bool(ID_C_java_generic_type);
+}
+
 /// \param type: the type to check
 /// \return true if type is java type containing with generics, e.g., List<T>
 inline bool is_java_generic_type(const typet &type)
 {
-  return type.get_bool(ID_C_java_generic_type);
+  return can_cast_type<java_generic_typet>(type);
 }
 
 /// \param type: source type
@@ -464,9 +470,7 @@ inline bool is_java_generic_type(const typet &type)
 inline const java_generic_typet &to_java_generic_type(
   const typet &type)
 {
-  PRECONDITION(
-    type.id()==ID_pointer &&
-    is_java_generic_type(type));
+  PRECONDITION(can_cast_type<java_generic_typet>(type));
   return static_cast<const java_generic_typet &>(type);
 }
 
@@ -474,9 +478,7 @@ inline const java_generic_typet &to_java_generic_type(
 /// \return cast of type into java type with generics
 inline java_generic_typet &to_java_generic_type(typet &type)
 {
-  PRECONDITION(
-    type.id()==ID_pointer &&
-    is_java_generic_type(type));
+  PRECONDITION(can_cast_type<java_generic_typet>(type));
   return static_cast<java_generic_typet &>(type);
 }