diff --git a/doc/cprover-manual/unsound_options.md b/doc/cprover-manual/unsound_options.md
index ebb3d290644..831f72456e8 100644
--- a/doc/cprover-manual/unsound_options.md
+++ b/doc/cprover-manual/unsound_options.md
@@ -36,6 +36,9 @@ The following options will produce a warning when used with CBMC or JBMC:
 See [Understanding Loop Unwinding](../cbmc/unwinding/) for an elaboration of
 these options.
 
+For arrays with unknown length (e.g. input arrays), JBMC has a default limit that
+can be changed with the option `--max-nondet-array-length`.
+
 ### Experimental Options
 
 Be advised that the following command line options to `cbmc` and `goto-instrument`
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
index 8eefa379e75..1142e1fee0c 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.h
+++ b/jbmc/src/java_bytecode/java_bytecode_language.h
@@ -63,7 +63,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "transform `throw` instructions into `assert FALSE` followed by " \
   "`assume FALSE`.\n" \
   " {y--max-nondet-array-length} {uN} \t " \
-  "limit nondet (e.g. input) array size to <= {uN}\n" \
+  "limit nondet (e.g. input) array size to <= {uN} (default 5)\n" \
   " {y--max-nondet-tree-depth} {uN} \t " \
   "limit size of nondet (e.g. input) object tree; at level {uN} references " \
   "are set to null\n" \