Limit string length to avoid spurious regression test failure

As seen in
https://github.com/diffblue/cbmc/actions/runs/4979949266/jobs/8933402303?pr=7413
we may end up with a counterexample too large store on GitHub's runner.
Limit the string length as the length is immaterial to the test.

Author: tautschnig

jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc

@@ -1,6 +1,6 @@
 CORE
 My
---function My.classArg --java-assume-inputs-non-null
+--function My.classArg --java-assume-inputs-non-null --max-nondet-string-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$