Set string-max-length in indexOf test

Without this, the solver can end up with a difficult instance for minisat.
This behavior depends on the envioronment in which CBMC/JBMC is build, for
instance travis and appVeyor may get different counter-examples from the
SAT-solver, because of slightly different inputs.
The behavior can also vary from one commit to the other on the same system (even
if the changes seem unrelated to the solvers).
However running the same benchmark on the same operating system with the same
version of CBMC/JBMC should always behave the same.

Author: romainbrenguier

regression/jbmc-strings/StringIndexOf/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --java-assume-inputs-non-null
+--refine-strings --function Test.check --unwind 4 --string-max-input-length 3 --string-max-length 100 --java-assume-inputs-non-null
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$