Merge pull request #8432 from lks9/doc_8428

add documentation of default for --max-nondet-array-length, see #8428

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`

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -63,7 +63,7 @@ Author: Daniel Kroening, [email protected]
   "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" \