diff --git a/src/java_bytecode/java_types.cpp b/src/java_bytecode/java_types.cpp
index 92b2ab27dcb..3f61e14ccba 100644
--- a/src/java_bytecode/java_types.cpp
+++ b/src/java_bytecode/java_types.cpp
@@ -123,6 +123,17 @@ reference_typet java_array_type(const char subtype)
   return java_reference_type(symbol_type);
 }
 
+/// Return the type of the elements of a given java array type
+/// \param array_type The java array type
+/// \return The type of the elements of the array
+typet java_array_element_type(const symbol_typet &array_type)
+{
+  INVARIANT(
+    is_java_array_tag(array_type.get_identifier()),
+    "Symbol should have array tag");
+  return array_type.find_type(ID_C_element_type);
+}
+
 /// See above
 /// \par parameters: Struct tag 'tag'
 /// \return True if the given struct is a Java array
diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h
index a51a6c3db95..740d347feb7 100644
--- a/src/java_bytecode/java_types.h
+++ b/src/java_bytecode/java_types.h
@@ -56,6 +56,7 @@ reference_typet java_lang_object_type();
 symbol_typet java_classname(const std::string &);
 
 reference_typet java_array_type(const char subtype);
+typet java_array_element_type(const symbol_typet &array_type);
 
 bool is_reference_type(char t);