Update strings regression tests

Author: svorenova

jbmc/regression/jbmc-strings/StringContains03/test.desc

@@ -1,11 +1,11 @@
 CORE
 Test.class
---function Test.check
+--function Test.check --max-nondet-string-length 1000000000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 file Test.java line 20 .*: FAILURE$
 --
 --
---max-nondet-string-length is not used on purpose, because this tests the behaviour
-of string refinement on very large strings.
+This tests the behaviour of string refinement on very large strings.
+max-nondet-string-length is set big enough to cause an overflow.

jbmc/regression/jbmc-strings/long_string/test_abort.desc

@@ -1,10 +1,11 @@
 CORE
 Test.class
---function Test.checkAbort --trace
+--function Test.checkAbort --trace --max-nondet-string-length 1000000000
 ^EXIT=10$
 ^SIGNAL=0$
 dynamic_object[0-9]*=\(assignment removed\)
 --
 --
 This tests that the object does not appear in the trace, because concretizing
 a string of the required length may take too much memory.
+max-nondet-string-length is set big enough to cause an overflow.

jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---function Test.checkMinLength --string-non-empty
+--function Test.checkMinLength --string-non-empty --max-nondet-string-length 2000000000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS
@@ -9,3 +9,5 @@ assertion.* line 17 function java::Test.checkMinLength.*: FAILURE
 assertion.* line 19 function java::Test.checkMinLength.*: FAILURE
 --
 ^Building error trace
+--
+max-nondet-string-length is set big enough to cause an overflow.