diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
index c44c000b141..08492cf5592 100644
--- a/jbmc/src/java_bytecode/java_types.cpp
+++ b/jbmc/src/java_bytecode/java_types.cpp
@@ -939,6 +939,8 @@ optionalt<size_t> java_generic_symbol_typet::generic_type_index(
 
 std::string pretty_java_type(const typet &type)
 {
+  if(type == java_void_type())
+    return "void";
   if(type == java_int_type())
     return "int";
   else if(type == java_long_type())
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index 0ca7538e95a..7e96efb02a2 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -306,6 +306,7 @@ typet java_char_type();
 typet java_float_type();
 typet java_double_type();
 typet java_boolean_type();
+typet java_void_type();
 reference_typet java_reference_type(const typet &subtype);
 reference_typet java_lang_object_type();
 symbol_typet java_classname(const std::string &);