CORE
Test.class
--verbosity 10 --max-nondet-string-length 500000 --function Test.checkMaxInputLength
^EXIT=10$
^SIGNAL=0$
assertion.* line 9 function java::Test.checkMaxInputLength.* bytecode-index 17: FAILURE
