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 --no-refine-strings
 ^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.
+--max-nondet-string-length is not bounded when --no-refine-strings is given,
+this tests the behaviour of string refinement on very large strings.

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

@@ -1,10 +1,11 @@
 CORE
 Test.class
---function Test.checkAbort --trace
+--function Test.checkAbort --trace --no-refine-strings
 ^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.
+a string of the required length may take too much memory. --no-refine-strings
+ensures that max-nondet-string-length is not bounded

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 --no-refine-strings
 ^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
+--
+--no-refine-strings ensures that max-nondet-string-length is not bounded