diff --git a/regression/strings-smoke-tests/java_append_int/test.desc b/regression/strings-smoke-tests/java_append_int/test.desc
index e1455859470..17f38286a5b 100644
--- a/regression/strings-smoke-tests/java_append_int/test.desc
+++ b/regression/strings-smoke-tests/java_append_int/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test_append_int.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_append_object/test.desc b/regression/strings-smoke-tests/java_append_object/test.desc
index 787852963ed..62c1f56eea2 100644
--- a/regression/strings-smoke-tests/java_append_object/test.desc
+++ b/regression/strings-smoke-tests/java_append_object/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test_append_object.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_append_string/test.desc b/regression/strings-smoke-tests/java_append_string/test.desc
index 943ca820bcc..39c04f7031d 100644
--- a/regression/strings-smoke-tests/java_append_string/test.desc
+++ b/regression/strings-smoke-tests/java_append_string/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_append_string.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_char_array/test.desc b/regression/strings-smoke-tests/java_char_array/test.desc
index d00a921a8c1..5c8a13eddd3 100644
--- a/regression/strings-smoke-tests/java_char_array/test.desc
+++ b/regression/strings-smoke-tests/java_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_char_array.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 .*assertion.* test_char_array.java line 9 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_char_array_init/test.desc b/regression/strings-smoke-tests/java_char_array_init/test.desc
index 04096a8a984..1202bb035b6 100644
--- a/regression/strings-smoke-tests/java_char_array_init/test.desc
+++ b/regression/strings-smoke-tests/java_char_array_init/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test_init.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_char_at/test.desc b/regression/strings-smoke-tests/java_char_at/test.desc
index f2d5ecad6c7..2be2ab204ca 100644
--- a/regression/strings-smoke-tests/java_char_at/test.desc
+++ b/regression/strings-smoke-tests/java_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_char_at.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_code_point/test.desc b/regression/strings-smoke-tests/java_code_point/test.desc
index e3be9616fa5..aa7799f5170 100644
--- a/regression/strings-smoke-tests/java_code_point/test.desc
+++ b/regression/strings-smoke-tests/java_code_point/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_code_point.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_compare/test.desc b/regression/strings-smoke-tests/java_compare/test.desc
index 9e6810476b9..a7d8151b55b 100644
--- a/regression/strings-smoke-tests/java_compare/test.desc
+++ b/regression/strings-smoke-tests/java_compare/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_compare.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_concat/test.desc b/regression/strings-smoke-tests/java_concat/test.desc
index 2dcca464779..6063f361aa5 100644
--- a/regression/strings-smoke-tests/java_concat/test.desc
+++ b/regression/strings-smoke-tests/java_concat/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_concat.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 10.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_delete/test.desc b/regression/strings-smoke-tests/java_delete/test.desc
index f0c0aedda91..dd957dd16bd 100644
--- a/regression/strings-smoke-tests/java_delete/test.desc
+++ b/regression/strings-smoke-tests/java_delete/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_delete_char_at/test.desc b/regression/strings-smoke-tests/java_delete_char_at/test.desc
index d415d16e9b6..cfd8b4778d1 100644
--- a/regression/strings-smoke-tests/java_delete_char_at/test.desc
+++ b/regression/strings-smoke-tests/java_delete_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete_char_at.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_empty/test.desc b/regression/strings-smoke-tests/java_empty/test.desc
index 181ff4ee5fd..e82479e301b 100644
--- a/regression/strings-smoke-tests/java_empty/test.desc
+++ b/regression/strings-smoke-tests/java_empty/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_empty.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_float/test.desc b/regression/strings-smoke-tests/java_float/test.desc
index 427d1fca836..5f225af821a 100644
--- a/regression/strings-smoke-tests/java_float/test.desc
+++ b/regression/strings-smoke-tests/java_float/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test_float.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_hash_code/test.desc b/regression/strings-smoke-tests/java_hash_code/test.desc
index fc628393186..c00e466b8c4 100644
--- a/regression/strings-smoke-tests/java_hash_code/test.desc
+++ b/regression/strings-smoke-tests/java_hash_code/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_hash_code.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_index_of/test.desc b/regression/strings-smoke-tests/java_index_of/test.desc
index e0e7de66561..3fdfa1ffc5d 100644
--- a/regression/strings-smoke-tests/java_index_of/test.desc
+++ b/regression/strings-smoke-tests/java_index_of/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_index_of2/test.desc b/regression/strings-smoke-tests/java_index_of2/test.desc
index 09a7398d4b7..2c9d464054c 100644
--- a/regression/strings-smoke-tests/java_index_of2/test.desc
+++ b/regression/strings-smoke-tests/java_index_of2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings-smoke-tests/java_index_of_char/test.desc b/regression/strings-smoke-tests/java_index_of_char/test.desc
index a95467b52e4..59d3310fa48 100644
--- a/regression/strings-smoke-tests/java_index_of_char/test.desc
+++ b/regression/strings-smoke-tests/java_index_of_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test1.desc b/regression/strings-smoke-tests/java_int_to_string/test1.desc
index 88f39d5eb12..318ec0fb224 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test2.desc b/regression/strings-smoke-tests/java_int_to_string/test2.desc
index 5ff465a846e..186a25d2d8b 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test2.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc
new file mode 100644
index 00000000000..00047bad217
--- /dev/null
+++ b/regression/strings-smoke-tests/java_int_to_string/test2_bug.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+Test2.class
+--refine-strings
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 7 .* SUCCESS$
+assertion.* line 10 .* FAILURE$
+--
+--
+When string-max-length is not set, the solver can run out of memory in
+an unpredictable way.
\ No newline at end of file
diff --git a/regression/strings-smoke-tests/java_int_to_string/test4.desc b/regression/strings-smoke-tests/java_int_to_string/test4.desc
index 2106e2defa5..abba00197d9 100644
--- a/regression/strings-smoke-tests/java_int_to_string/test4.desc
+++ b/regression/strings-smoke-tests/java_int_to_string/test4.desc
@@ -1,6 +1,6 @@
 CORE
 Test4.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc b/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
index b1ed3bac24c..416e3caec69 100644
--- a/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_knownbug/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
index a4e6438623e..c24b0bbd20b 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_binary3.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary3.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
index 7226334925f..de106c0cbf5 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_decimal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
index 9afe7b06279..f4b1e2b219d 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal1.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
index d8959c329a7..20efbdfa239 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_binary.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test_binary.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
index 324cd50051e..69dbaba276d 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_hex.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test_hex.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
index ce0a5607186..7cfc1c19f24 100644
--- a/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
+++ b/regression/strings-smoke-tests/java_int_to_string_with_radix_knownbug/test_octal.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test_octal.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_intern/test.desc b/regression/strings-smoke-tests/java_intern/test.desc
index c8d0eea43bd..58c51bce301 100644
--- a/regression/strings-smoke-tests/java_intern/test.desc
+++ b/regression/strings-smoke-tests/java_intern/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_intern.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_last_index_of/test.desc b/regression/strings-smoke-tests/java_last_index_of/test.desc
index 381078254cd..afda4875b71 100644
--- a/regression/strings-smoke-tests/java_last_index_of/test.desc
+++ b/regression/strings-smoke-tests/java_last_index_of/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_last_index_of.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_last_index_of2/test.desc b/regression/strings-smoke-tests/java_last_index_of2/test.desc
index 5348cbe7fce..28af8ca48e6 100644
--- a/regression/strings-smoke-tests/java_last_index_of2/test.desc
+++ b/regression/strings-smoke-tests/java_last_index_of2/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_last_index_of2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_last_index_of_char/test.desc b/regression/strings-smoke-tests/java_last_index_of_char/test.desc
index aa88fc5f6ef..aa59690787c 100644
--- a/regression/strings-smoke-tests/java_last_index_of_char/test.desc
+++ b/regression/strings-smoke-tests/java_last_index_of_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_last_index_of_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_length/test.desc b/regression/strings-smoke-tests/java_length/test.desc
index 60c360eecb8..7802a6d675b 100644
--- a/regression/strings-smoke-tests/java_length/test.desc
+++ b/regression/strings-smoke-tests/java_length/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_length.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings-smoke-tests/java_length2/test.desc b/regression/strings-smoke-tests/java_length2/test.desc
index e473b51d950..4647009f3cf 100644
--- a/regression/strings-smoke-tests/java_length2/test.desc
+++ b/regression/strings-smoke-tests/java_length2/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.class
---refine-strings --function test.check
+--refine-strings --string-max-length 1000 --function test.check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test1.desc b/regression/strings-smoke-tests/java_long_to_string/test1.desc
index 88f39d5eb12..318ec0fb224 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test2.desc b/regression/strings-smoke-tests/java_long_to_string/test2.desc
index a4f7d628251..1f6206fafd9 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test2.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test3.desc b/regression/strings-smoke-tests/java_long_to_string/test3.desc
index 5e96ef2ae6d..ea8df93a51f 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test3.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test3.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test4.desc b/regression/strings-smoke-tests/java_long_to_string/test4.desc
index aa12d7732f1..13dd59d749e 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test4.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test4.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test4.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string/test5.desc b/regression/strings-smoke-tests/java_long_to_string/test5.desc
index 08531bc36e0..524a176db3f 100644
--- a/regression/strings-smoke-tests/java_long_to_string/test5.desc
+++ b/regression/strings-smoke-tests/java_long_to_string/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
index bfdddd48786..6f9c074face 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test_binary1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
index 7cabc082721..0729b99b895 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test_binary2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
index cd10cf15647..d87aaaecb3d 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary3.desc
@@ -1,6 +1,6 @@
 THOROUGH
 Test_binary3.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
index 7226334925f..de106c0cbf5 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_decimal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
index d21d067e620..89c4928e147 100644
--- a/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
+++ b/regression/strings-smoke-tests/java_long_to_string_with_radix/test_hex2.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_object_allocation/test.desc b/regression/strings-smoke-tests/java_object_allocation/test.desc
index fe10bf71202..bac94ff5307 100644
--- a/regression/strings-smoke-tests/java_object_allocation/test.desc
+++ b/regression/strings-smoke-tests/java_object_allocation/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --show-goto-functions
+--refine-strings --string-max-length 1000 --show-goto-functions
 // Enable multi-line checking
 activate-multi-line-match
 EXIT=0
diff --git a/regression/strings-smoke-tests/java_parseint/test1.desc b/regression/strings-smoke-tests/java_parseint/test1.desc
index 5d48a0d6aad..5307e54205f 100644
--- a/regression/strings-smoke-tests/java_parseint/test1.desc
+++ b/regression/strings-smoke-tests/java_parseint/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint/test2.desc b/regression/strings-smoke-tests/java_parseint/test2.desc
index 16f6de423bf..b61e0912459 100644
--- a/regression/strings-smoke-tests/java_parseint/test2.desc
+++ b/regression/strings-smoke-tests/java_parseint/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint/test3.desc b/regression/strings-smoke-tests/java_parseint/test3.desc
index bb643427dd2..06f5f081dfd 100644
--- a/regression/strings-smoke-tests/java_parseint/test3.desc
+++ b/regression/strings-smoke-tests/java_parseint/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* FAILURE$
diff --git a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
index 76feb55c355..f66e48584e2 100644
--- a/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_parseint_knownbug/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 10.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
index 0ab380c3cde..07502efb78d 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test1.desc
@@ -1,6 +1,6 @@
 CORE
 Test1.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
index 0b6a1a2dd97..0755c7a91cf 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test2.desc
@@ -1,6 +1,6 @@
 CORE
 Test2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
index 7b68147d90b..ef8136a08ab 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test3.desc
@@ -1,6 +1,6 @@
 CORE
 Test3.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
index 8c775500aaa..7934721b588 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test4.desc
@@ -1,6 +1,6 @@
 CORE
 Test4.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
index 2b0338b1c0c..a829acab959 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test5.desc
@@ -1,6 +1,6 @@
 CORE
 Test5.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc b/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
index 71b3d8423e4..d3dadcebc8f 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix/test6.desc
@@ -1,6 +1,6 @@
 CORE
 Test6.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
index b0af402d3bd..485ca577bcc 100644
--- a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
+++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test2.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_binary_min.desc b/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
index 9fa189f76cf..ce64f5e6db6 100644
--- a/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_binary_min.desc
@@ -1,6 +1,6 @@
 CORE
 Test_binary_min.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc b/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
index 25795287397..1e195fcaaf2 100644
--- a/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_decimal_max.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal_max.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc b/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
index 95a847bf862..7f97fa3a95e 100644
--- a/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_decimal_min.desc
@@ -1,6 +1,6 @@
 CORE
 Test_decimal_min.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_hex.desc b/regression/strings-smoke-tests/java_parselong/test_hex.desc
index efae1994f9e..c21910790b5 100644
--- a/regression/strings-smoke-tests/java_parselong/test_hex.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_hex.desc
@@ -1,6 +1,6 @@
 CORE
 Test_hex.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_parselong/test_octal.desc b/regression/strings-smoke-tests/java_parselong/test_octal.desc
index 72dc00545cb..152484b2d2a 100644
--- a/regression/strings-smoke-tests/java_parselong/test_octal.desc
+++ b/regression/strings-smoke-tests/java_parselong/test_octal.desc
@@ -1,6 +1,6 @@
 CORE
 Test_octal.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_replace_char/test.desc b/regression/strings-smoke-tests/java_replace_char/test.desc
index 5c336326e5d..9cf3b2fbced 100644
--- a/regression/strings-smoke-tests/java_replace_char/test.desc
+++ b/regression/strings-smoke-tests/java_replace_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_replace_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_set_char_at/test.desc b/regression/strings-smoke-tests/java_set_char_at/test.desc
index 1c471d0194a..72f26dda255 100644
--- a/regression/strings-smoke-tests/java_set_char_at/test.desc
+++ b/regression/strings-smoke-tests/java_set_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_set_char_at.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_starts_with/test.desc b/regression/strings-smoke-tests/java_starts_with/test.desc
index ec6b84102f2..5c62d2f2718 100644
--- a/regression/strings-smoke-tests/java_starts_with/test.desc
+++ b/regression/strings-smoke-tests/java_starts_with/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_starts_with.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_string_builder_length/test.desc b/regression/strings-smoke-tests/java_string_builder_length/test.desc
index 2a37e02a36c..3ad293630e3 100644
--- a/regression/strings-smoke-tests/java_string_builder_length/test.desc
+++ b/regression/strings-smoke-tests/java_string_builder_length/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_sb_length.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_subsequence/test.desc b/regression/strings-smoke-tests/java_subsequence/test.desc
index df3cc28619f..3f4941d15dd 100644
--- a/regression/strings-smoke-tests/java_subsequence/test.desc
+++ b/regression/strings-smoke-tests/java_subsequence/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_subsequence.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_substring/test.desc b/regression/strings-smoke-tests/java_substring/test.desc
index 26ec800cfac..9faeee00d73 100644
--- a/regression/strings-smoke-tests/java_substring/test.desc
+++ b/regression/strings-smoke-tests/java_substring/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_substring.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings-smoke-tests/java_value_of_float_3/test.desc b/regression/strings-smoke-tests/java_value_of_float_3/test.desc
index 771fdebe7cc..2c28aafd4d9 100644
--- a/regression/strings-smoke-tests/java_value_of_float_3/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float_3/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 test.class
---refine-strings --function test.check
+--refine-strings --string-max-length 1000 --function test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 7 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.desc b/regression/strings-smoke-tests/java_value_of_float_4/test.desc
index 7f1e0f8819a..a85559c560e 100644
--- a/regression/strings-smoke-tests/java_value_of_float_4/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float_4/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 test.class
---refine-strings --function test.check
+--refine-strings --string-max-length 1000 --function test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* test.java line 8 .* SUCCESS$
diff --git a/regression/strings-smoke-tests/java_value_of_float_5/test.desc b/regression/strings-smoke-tests/java_value_of_float_5/test.desc
index 7a279ade453..07a7bd7edde 100644
--- a/regression/strings-smoke-tests/java_value_of_float_5/test.desc
+++ b/regression/strings-smoke-tests/java_value_of_float_5/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 test.class
---refine-strings --function test.check
+--refine-strings --string-max-length 1000 --function test.check
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 6 .* SUCCESS$
diff --git a/regression/strings/CharacterGetNumericValue/test.desc b/regression/strings/CharacterGetNumericValue/test.desc
index 9f34df46fd6..30ce2644914 100644
--- a/regression/strings/CharacterGetNumericValue/test.desc
+++ b/regression/strings/CharacterGetNumericValue/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion at file test.java line 8 .* SUCCESS$
diff --git a/regression/strings/RegexMatches01/test.desc b/regression/strings/RegexMatches01/test.desc
index e4259466e6b..4a95eb71ab0 100644
--- a/regression/strings/RegexMatches01/test.desc
+++ b/regression/strings/RegexMatches01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegexMatches01.class
---refine-strings --unwind 100
+--refine-strings --string-max-length 1000 --unwind 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/RegexMatches02/test.desc b/regression/strings/RegexMatches02/test.desc
index 006922c3d6a..9b754d1a449 100644
--- a/regression/strings/RegexMatches02/test.desc
+++ b/regression/strings/RegexMatches02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegexMatches02.class
---refine-strings --unwind 100
+--refine-strings --string-max-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/RegexSubstitution01/test.desc b/regression/strings/RegexSubstitution01/test.desc
index ccf24b2e8fa..2d24db23d16 100644
--- a/regression/strings/RegexSubstitution01/test.desc
+++ b/regression/strings/RegexSubstitution01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/RegexSubstitution02/test.desc b/regression/strings/RegexSubstitution02/test.desc
index 7064bcc0333..2caa11a3221 100644
--- a/regression/strings/RegexSubstitution02/test.desc
+++ b/regression/strings/RegexSubstitution02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/RegexSubstitution03/test.desc b/regression/strings/RegexSubstitution03/test.desc
index 4b0d5739c42..9f141b34217 100644
--- a/regression/strings/RegexSubstitution03/test.desc
+++ b/regression/strings/RegexSubstitution03/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegexSubstitution03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StaticCharMethods01/test.desc b/regression/strings/StaticCharMethods01/test.desc
index 0440fc98273..35c0f3a7f1e 100644
--- a/regression/strings/StaticCharMethods01/test.desc
+++ b/regression/strings/StaticCharMethods01/test.desc
@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StaticCharMethods02/test.desc b/regression/strings/StaticCharMethods02/test.desc
index d537da812c9..70e90e4115a 100644
--- a/regression/strings/StaticCharMethods02/test.desc
+++ b/regression/strings/StaticCharMethods02/test.desc
@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StaticCharMethods03/test.desc b/regression/strings/StaticCharMethods03/test.desc
index 174071ed1da..712044431a5 100644
--- a/regression/strings/StaticCharMethods03/test.desc
+++ b/regression/strings/StaticCharMethods03/test.desc
@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 6 .* FAILURE$
diff --git a/regression/strings/StaticCharMethods04/test.desc b/regression/strings/StaticCharMethods04/test.desc
index ecc807f2d31..ee66116b0fa 100644
--- a/regression/strings/StaticCharMethods04/test.desc
+++ b/regression/strings/StaticCharMethods04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods04.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StaticCharMethods05/test.desc b/regression/strings/StaticCharMethods05/test.desc
index f8abd67fc57..e6f2a0e6ee8 100644
--- a/regression/strings/StaticCharMethods05/test.desc
+++ b/regression/strings/StaticCharMethods05/test.desc
@@ -1,6 +1,6 @@
 CORE
 StaticCharMethods05.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 null-pointer-exception\.14\] Throw null: FAILURE
diff --git a/regression/strings/StaticCharMethods06/test.desc b/regression/strings/StaticCharMethods06/test.desc
index 3caa6a7b878..b0047376ea1 100644
--- a/regression/strings/StaticCharMethods06/test.desc
+++ b/regression/strings/StaticCharMethods06/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StaticCharMethods06.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringBuilderAppend01/test.desc b/regression/strings/StringBuilderAppend01/test.desc
index d0207fc9ea7..925b862d11e 100644
--- a/regression/strings/StringBuilderAppend01/test.desc
+++ b/regression/strings/StringBuilderAppend01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderAppend01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringBuilderAppend02/test.desc b/regression/strings/StringBuilderAppend02/test.desc
index 70357b670d8..d0ef683f373 100644
--- a/regression/strings/StringBuilderAppend02/test.desc
+++ b/regression/strings/StringBuilderAppend02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderAppend02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderCapLen01/test.desc b/regression/strings/StringBuilderCapLen01/test.desc
index 4186f2534ac..12d6f321534 100644
--- a/regression/strings/StringBuilderCapLen01/test.desc
+++ b/regression/strings/StringBuilderCapLen01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringBuilderCapLen02/test.desc b/regression/strings/StringBuilderCapLen02/test.desc
index f9db006ed0b..68183ab0c8b 100644
--- a/regression/strings/StringBuilderCapLen02/test.desc
+++ b/regression/strings/StringBuilderCapLen02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderCapLen03/test.desc b/regression/strings/StringBuilderCapLen03/test.desc
index c35dfb33871..98f5aa74306 100644
--- a/regression/strings/StringBuilderCapLen03/test.desc
+++ b/regression/strings/StringBuilderCapLen03/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderCapLen04/test.desc b/regression/strings/StringBuilderCapLen04/test.desc
index 78930851e45..2bf31910709 100644
--- a/regression/strings/StringBuilderCapLen04/test.desc
+++ b/regression/strings/StringBuilderCapLen04/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderCapLen04.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderChars01/test.desc b/regression/strings/StringBuilderChars01/test.desc
index 48acfb25a5d..df8aa84cc74 100644
--- a/regression/strings/StringBuilderChars01/test.desc
+++ b/regression/strings/StringBuilderChars01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars01.class
---refine-strings --unwind 100
+--refine-strings --string-max-length 1000 --unwind 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringBuilderChars02/test.desc b/regression/strings/StringBuilderChars02/test.desc
index d9006ab74ba..991d4cca0eb 100644
--- a/regression/strings/StringBuilderChars02/test.desc
+++ b/regression/strings/StringBuilderChars02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars02.class
---refine-strings --unwind 100
+--refine-strings --string-max-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderChars03/test.desc b/regression/strings/StringBuilderChars03/test.desc
index d6f1cb4155c..6ec91ba3f69 100644
--- a/regression/strings/StringBuilderChars03/test.desc
+++ b/regression/strings/StringBuilderChars03/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars03.class
---refine-strings --unwind 100
+--refine-strings --string-max-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderChars04/test.desc b/regression/strings/StringBuilderChars04/test.desc
index 37009795a48..802a60269ec 100644
--- a/regression/strings/StringBuilderChars04/test.desc
+++ b/regression/strings/StringBuilderChars04/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars04.class
---refine-strings --unwind 100
+--refine-strings --string-max-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderChars05/test.desc b/regression/strings/StringBuilderChars05/test.desc
index 49aed9d48fd..fdb12721623 100644
--- a/regression/strings/StringBuilderChars05/test.desc
+++ b/regression/strings/StringBuilderChars05/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars05.class
---refine-strings --unwind 100
+--refine-strings --string-max-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderChars06/test.desc b/regression/strings/StringBuilderChars06/test.desc
index 5ccf470590e..fbb6f1bb87d 100644
--- a/regression/strings/StringBuilderChars06/test.desc
+++ b/regression/strings/StringBuilderChars06/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderChars06.class
---refine-strings --unwind 100
+--refine-strings --string-max-length 1000 --unwind 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderConstructors01/test.desc b/regression/strings/StringBuilderConstructors01/test.desc
index 3e27d46c329..39bcec0b205 100644
--- a/regression/strings/StringBuilderConstructors01/test.desc
+++ b/regression/strings/StringBuilderConstructors01/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 StringBuilderConstructors01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringBuilderConstructors02/test.desc b/regression/strings/StringBuilderConstructors02/test.desc
index f6c0cded34e..889460297ea 100644
--- a/regression/strings/StringBuilderConstructors02/test.desc
+++ b/regression/strings/StringBuilderConstructors02/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 StringBuilderConstructors02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderInsertDelete01/test.desc b/regression/strings/StringBuilderInsertDelete01/test.desc
index b2f927ad3b7..5c347f7792a 100644
--- a/regression/strings/StringBuilderInsertDelete01/test.desc
+++ b/regression/strings/StringBuilderInsertDelete01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderInsertDelete01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringBuilderInsertDelete02/test.desc b/regression/strings/StringBuilderInsertDelete02/test.desc
index 1e67f7eb3c0..576410049d8 100644
--- a/regression/strings/StringBuilderInsertDelete02/test.desc
+++ b/regression/strings/StringBuilderInsertDelete02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderInsertDelete02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringBuilderInsertDelete03/test.desc b/regression/strings/StringBuilderInsertDelete03/test.desc
index 084038f4465..934b4de8579 100644
--- a/regression/strings/StringBuilderInsertDelete03/test.desc
+++ b/regression/strings/StringBuilderInsertDelete03/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringBuilderInsertDelete03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringCompare01/test.desc b/regression/strings/StringCompare01/test.desc
index 2140f3a0c48..5e60d31b865 100644
--- a/regression/strings/StringCompare01/test.desc
+++ b/regression/strings/StringCompare01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringCompare01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringCompare02/test.desc b/regression/strings/StringCompare02/test.desc
index d20bfb7eb5c..2970a511914 100644
--- a/regression/strings/StringCompare02/test.desc
+++ b/regression/strings/StringCompare02/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringCompare02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$
diff --git a/regression/strings/StringCompare03/test.desc b/regression/strings/StringCompare03/test.desc
index afc9b9b5307..15b7f91b1fe 100644
--- a/regression/strings/StringCompare03/test.desc
+++ b/regression/strings/StringCompare03/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringCompare03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$
diff --git a/regression/strings/StringCompare04/test.desc b/regression/strings/StringCompare04/test.desc
index afc70f4933b..176142e064e 100644
--- a/regression/strings/StringCompare04/test.desc
+++ b/regression/strings/StringCompare04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringCompare04.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringCompare05/test.desc b/regression/strings/StringCompare05/test.desc
index 0f24821dee6..a182fecf008 100644
--- a/regression/strings/StringCompare05/test.desc
+++ b/regression/strings/StringCompare05/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringCompare05.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringConcatenation01/test.desc b/regression/strings/StringConcatenation01/test.desc
index 29244c24734..09414c5a3f6 100644
--- a/regression/strings/StringConcatenation01/test.desc
+++ b/regression/strings/StringConcatenation01/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringConcatenation01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringConcatenation02/test.desc b/regression/strings/StringConcatenation02/test.desc
index ad9402eaec9..90c299fea1a 100644
--- a/regression/strings/StringConcatenation02/test.desc
+++ b/regression/strings/StringConcatenation02/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringConcatenation02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringConcatenation03/test.desc b/regression/strings/StringConcatenation03/test.desc
index c5798d1ae1d..2dd24800903 100644
--- a/regression/strings/StringConcatenation03/test.desc
+++ b/regression/strings/StringConcatenation03/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringConcatenation03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringConcatenation04/test.desc b/regression/strings/StringConcatenation04/test.desc
index a781c7887b1..5fbdea80b8a 100644
--- a/regression/strings/StringConcatenation04/test.desc
+++ b/regression/strings/StringConcatenation04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringConcatenation04.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 8 .* FAILURE$
diff --git a/regression/strings/StringConstructors01/test.desc b/regression/strings/StringConstructors01/test.desc
index b1465868c19..6c3fdfb7af8 100644
--- a/regression/strings/StringConstructors01/test.desc
+++ b/regression/strings/StringConstructors01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringConstructors01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringConstructors02/test.desc b/regression/strings/StringConstructors02/test.desc
index 37838aafbc9..f39f6dbcf25 100644
--- a/regression/strings/StringConstructors02/test.desc
+++ b/regression/strings/StringConstructors02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringConstructors02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringConstructors03/test.desc b/regression/strings/StringConstructors03/test.desc
index 10193fc66c2..3df88975a3e 100644
--- a/regression/strings/StringConstructors03/test.desc
+++ b/regression/strings/StringConstructors03/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringConstructors03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringConstructors04/test.desc b/regression/strings/StringConstructors04/test.desc
index 2e6e88fa862..9e889d73812 100644
--- a/regression/strings/StringConstructors04/test.desc
+++ b/regression/strings/StringConstructors04/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringConstructors04.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringConstructors05/test.desc b/regression/strings/StringConstructors05/test.desc
index a3c6a6c0437..80b0ee57307 100644
--- a/regression/strings/StringConstructors05/test.desc
+++ b/regression/strings/StringConstructors05/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringConstructors05.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringContains01/test.desc b/regression/strings/StringContains01/test.desc
index 2e66f73126f..6a299037d6f 100644
--- a/regression/strings/StringContains01/test.desc
+++ b/regression/strings/StringContains01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringContains02/test.desc b/regression/strings/StringContains02/test.desc
index 2e66f73126f..6a299037d6f 100644
--- a/regression/strings/StringContains02/test.desc
+++ b/regression/strings/StringContains02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/StringIndexMethods01/test.desc b/regression/strings/StringIndexMethods01/test.desc
index 4bdc0d39b71..96c8fb19994 100644
--- a/regression/strings/StringIndexMethods01/test.desc
+++ b/regression/strings/StringIndexMethods01/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 StringIndexMethods01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringIndexMethods02/test.desc b/regression/strings/StringIndexMethods02/test.desc
index 05518537f78..69250ebae1d 100644
--- a/regression/strings/StringIndexMethods02/test.desc
+++ b/regression/strings/StringIndexMethods02/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringIndexMethods02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 6 .* FAILURE$
diff --git a/regression/strings/StringIndexMethods03/test.desc b/regression/strings/StringIndexMethods03/test.desc
index 17a62282b22..ce9b8e5a339 100644
--- a/regression/strings/StringIndexMethods03/test.desc
+++ b/regression/strings/StringIndexMethods03/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringIndexMethods03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 6 .* FAILURE$
diff --git a/regression/strings/StringIndexMethods04/StringIndexMethods04.class b/regression/strings/StringIndexMethods04/StringIndexMethods04.class
index 69a8fe4d628..10dc4401805 100644
Binary files a/regression/strings/StringIndexMethods04/StringIndexMethods04.class and b/regression/strings/StringIndexMethods04/StringIndexMethods04.class differ
diff --git a/regression/strings/StringIndexMethods04/StringIndexMethods04.java b/regression/strings/StringIndexMethods04/StringIndexMethods04.java
index 1271bcaf36b..2e5899aa25b 100644
--- a/regression/strings/StringIndexMethods04/StringIndexMethods04.java
+++ b/regression/strings/StringIndexMethods04/StringIndexMethods04.java
@@ -1,6 +1,12 @@
 public class StringIndexMethods04
 {
    public static void main(String[] args)
+   {
+      String letters = "onatdiffblue";
+      assert letters.indexOf("diffblue")==2;
+   }
+
+  public static void mainBug(String[] args)
    {
       String letters = "automatictestcasegenerationatdiffblue";
       assert letters.indexOf("diffblue")==28;
diff --git a/regression/strings/StringIndexMethods04/test.desc b/regression/strings/StringIndexMethods04/test.desc
index 5902a92be18..f63d2152f09 100644
--- a/regression/strings/StringIndexMethods04/test.desc
+++ b/regression/strings/StringIndexMethods04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringIndexMethods04.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 6 .* FAILURE$
diff --git a/regression/strings/StringIndexMethods04/test_bug.desc b/regression/strings/StringIndexMethods04/test_bug.desc
new file mode 100644
index 00000000000..ce351fe8d81
--- /dev/null
+++ b/regression/strings/StringIndexMethods04/test_bug.desc
@@ -0,0 +1,12 @@
+KNOWNBUG
+StringIndexMethods04.class
+--refine-strings --string-max-length 1000 --function StringIndexMethods04.mainBug
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion\.1\] .* line 6 .* FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+This test can randomly fail because the solver does not come up with the right
+model on the first iteration and the constraint instatiation adds too many things.
diff --git a/regression/strings/StringIndexMethods05/test.desc b/regression/strings/StringIndexMethods05/test.desc
index 29dee098ac7..243c43e965a 100644
--- a/regression/strings/StringIndexMethods05/test.desc
+++ b/regression/strings/StringIndexMethods05/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringIndexMethods05.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 6 .* FAILURE$
diff --git a/regression/strings/StringMiscellaneous01/test.desc b/regression/strings/StringMiscellaneous01/test.desc
index 624c8028cb3..6443a3f37d8 100644
--- a/regression/strings/StringMiscellaneous01/test.desc
+++ b/regression/strings/StringMiscellaneous01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringMiscellaneous01.class
---refine-strings --unwind 30
+--refine-strings --string-max-length 1000 --unwind 30
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringMiscellaneous02/test.desc b/regression/strings/StringMiscellaneous02/test.desc
index 7fd0118b93a..987299cb4af 100644
--- a/regression/strings/StringMiscellaneous02/test.desc
+++ b/regression/strings/StringMiscellaneous02/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringMiscellaneous02.class
---refine-strings --unwind 30
+--refine-strings --string-max-length 1000 --unwind 30
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 6 .* FAILURE$
diff --git a/regression/strings/StringMiscellaneous03/test.desc b/regression/strings/StringMiscellaneous03/test.desc
index d19fcdfaa5e..7a20ece6152 100644
--- a/regression/strings/StringMiscellaneous03/test.desc
+++ b/regression/strings/StringMiscellaneous03/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringMiscellaneous03.class
---refine-strings --unwind 30
+--refine-strings --string-max-length 1000 --unwind 30
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 11 .* FAILURE$
diff --git a/regression/strings/StringMiscellaneous04/test.desc b/regression/strings/StringMiscellaneous04/test.desc
index 9eb355cd0d2..5657433d8c7 100644
--- a/regression/strings/StringMiscellaneous04/test.desc
+++ b/regression/strings/StringMiscellaneous04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringMiscellaneous04.class
---refine-strings --unwind 30
+--refine-strings --string-max-length 1000 --unwind 30
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringStartEnd01/test.desc b/regression/strings/StringStartEnd01/test.desc
index 123429bd623..21181368d56 100644
--- a/regression/strings/StringStartEnd01/test.desc
+++ b/regression/strings/StringStartEnd01/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 StringStartEnd01.class
---refine-strings --unwind 30
+--refine-strings --string-max-length 1000 --unwind 30
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringStartEnd03/test.desc b/regression/strings/StringStartEnd03/test.desc
index b7727fd8b91..ad05b3a1904 100644
--- a/regression/strings/StringStartEnd03/test.desc
+++ b/regression/strings/StringStartEnd03/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 StringStartEnd03.class
---refine-strings --unwind 15
+--refine-strings --string-max-length 1000 --unwind 15
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 13 .* FAILURE$
diff --git a/regression/strings/StringValueOf01/test.desc b/regression/strings/StringValueOf01/test.desc
index c6098401ba0..19dc04f76f3 100644
--- a/regression/strings/StringValueOf01/test.desc
+++ b/regression/strings/StringValueOf01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringValueOf01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/StringValueOf02/test.desc b/regression/strings/StringValueOf02/test.desc
index 906d983e34f..3640d830371 100644
--- a/regression/strings/StringValueOf02/test.desc
+++ b/regression/strings/StringValueOf02/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/regression/strings/StringValueOf03/test.desc b/regression/strings/StringValueOf03/test.desc
index ffde4e2de6f..788c99b840c 100644
--- a/regression/strings/StringValueOf03/test.desc
+++ b/regression/strings/StringValueOf03/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/regression/strings/StringValueOf04/test.desc b/regression/strings/StringValueOf04/test.desc
index e73f1492261..1628779f989 100644
--- a/regression/strings/StringValueOf04/test.desc
+++ b/regression/strings/StringValueOf04/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf04.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/regression/strings/StringValueOf05/test.desc b/regression/strings/StringValueOf05/test.desc
index 494b6779cc2..281e1787b98 100644
--- a/regression/strings/StringValueOf05/test.desc
+++ b/regression/strings/StringValueOf05/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf05.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/regression/strings/StringValueOf06/test.desc b/regression/strings/StringValueOf06/test.desc
index 29fe55a89f2..23d219415d2 100644
--- a/regression/strings/StringValueOf06/test.desc
+++ b/regression/strings/StringValueOf06/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf06.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/regression/strings/StringValueOf07/test.desc b/regression/strings/StringValueOf07/test.desc
index e1d94ae7025..af73181177d 100644
--- a/regression/strings/StringValueOf07/test.desc
+++ b/regression/strings/StringValueOf07/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOf07.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 8 .* FAILURE$
diff --git a/regression/strings/StringValueOf09/test.desc b/regression/strings/StringValueOf09/test.desc
index d1bad9a12b6..d3387709636 100644
--- a/regression/strings/StringValueOf09/test.desc
+++ b/regression/strings/StringValueOf09/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 StringValueOf09.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/regression/strings/StringValueOf10/test.desc b/regression/strings/StringValueOf10/test.desc
index 3f8c5d6d60f..90a38f97794 100644
--- a/regression/strings/StringValueOf10/test.desc
+++ b/regression/strings/StringValueOf10/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 StringValueOf10.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/SubString01/test.desc b/regression/strings/SubString01/test.desc
index 975eaa118f3..f77f04ee2c7 100644
--- a/regression/strings/SubString01/test.desc
+++ b/regression/strings/SubString01/test.desc
@@ -1,6 +1,6 @@
 CORE
 SubString01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/SubString02/test.desc b/regression/strings/SubString02/test.desc
index 2003191a147..c487dd9ab17 100644
--- a/regression/strings/SubString02/test.desc
+++ b/regression/strings/SubString02/test.desc
@@ -1,6 +1,6 @@
 CORE
 SubString02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/regression/strings/SubString03/test.desc b/regression/strings/SubString03/test.desc
index 22143857480..48075842027 100644
--- a/regression/strings/SubString03/test.desc
+++ b/regression/strings/SubString03/test.desc
@@ -1,6 +1,6 @@
 CORE
 SubString03.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 7 .* FAILURE$
diff --git a/regression/strings/TokenTest01/test.desc b/regression/strings/TokenTest01/test.desc
index 122e6a8830a..921e312b85e 100644
--- a/regression/strings/TokenTest01/test.desc
+++ b/regression/strings/TokenTest01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 TokenTest01.class
---refine-strings --unwind 30
+--refine-strings --string-max-length 1000 --unwind 30
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/TokenTest02/test.desc b/regression/strings/TokenTest02/test.desc
index 6d1dabed602..0cc1d6a0d26 100644
--- a/regression/strings/TokenTest02/test.desc
+++ b/regression/strings/TokenTest02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 TokenTest02.class
---refine-strings --unwind 15
+--refine-strings --string-max-length 1000 --unwind 15
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/Validate01/test.desc b/regression/strings/Validate01/test.desc
index 649136a2956..7893ef03d1b 100644
--- a/regression/strings/Validate01/test.desc
+++ b/regression/strings/Validate01/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 Validate01.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/Validate02/test.desc b/regression/strings/Validate02/test.desc
index 22251c38a95..36385610844 100644
--- a/regression/strings/Validate02/test.desc
+++ b/regression/strings/Validate02/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 Validate02.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/bug-test-gen-095/test.desc b/regression/strings/bug-test-gen-095/test.desc
index 9f39bb3f26c..9c690be3298 100644
--- a/regression/strings/bug-test-gen-095/test.desc
+++ b/regression/strings/bug-test-gen-095/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 \[.*assertion\.1\] .* line 8 .* FAILURE
diff --git a/regression/strings/bug-test-gen-119-2/test.desc b/regression/strings/bug-test-gen-119-2/test.desc
index 312601b835d..447be05df73 100644
--- a/regression/strings/bug-test-gen-119-2/test.desc
+++ b/regression/strings/bug-test-gen-119-2/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOfLong.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/bug-test-gen-119/test.desc b/regression/strings/bug-test-gen-119/test.desc
index c5672ad9702..22bd78b3cac 100644
--- a/regression/strings/bug-test-gen-119/test.desc
+++ b/regression/strings/bug-test-gen-119/test.desc
@@ -1,6 +1,6 @@
 CORE
 StringValueOfBool.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/java_append_int/test.desc b/regression/strings/java_append_int/test.desc
index 1d3e387d278..8edf69c9fec 100644
--- a/regression/strings/java_append_int/test.desc
+++ b/regression/strings/java_append_int/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 test_append_int.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 9.* FAILURE$
diff --git a/regression/strings/java_append_object/test.desc b/regression/strings/java_append_object/test.desc
index 23ad1a81be4..2af06f2686a 100644
--- a/regression/strings/java_append_object/test.desc
+++ b/regression/strings/java_append_object/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 test_append_object.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 15.* FAILURE$
diff --git a/regression/strings/java_append_string/test.desc b/regression/strings/java_append_string/test.desc
index 7b6ea8ccae7..cb881ab83d9 100644
--- a/regression/strings/java_append_string/test.desc
+++ b/regression/strings/java_append_string/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test_append_string.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 12.* FAILURE$
diff --git a/regression/strings/java_char_array/test.desc b/regression/strings/java_char_array/test.desc
index 0acb4c57e47..aaf2c9f8fd4 100644
--- a/regression/strings/java_char_array/test.desc
+++ b/regression/strings/java_char_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_char_array.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 9.* FAILURE$
diff --git a/regression/strings/java_char_at/test.desc b/regression/strings/java_char_at/test.desc
index b9f7706b7e2..dd2c1c343ae 100644
--- a/regression/strings/java_char_at/test.desc
+++ b/regression/strings/java_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_char_at.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 5.* FAILURE$
diff --git a/regression/strings/java_code_point/test.desc b/regression/strings/java_code_point/test.desc
index b8571739ab9..322ead7c0a1 100644
--- a/regression/strings/java_code_point/test.desc
+++ b/regression/strings/java_code_point/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_code_point.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/regression/strings/java_compare/test.desc b/regression/strings/java_compare/test.desc
index c409e58fadc..6b8c890288d 100644
--- a/regression/strings/java_compare/test.desc
+++ b/regression/strings/java_compare/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_compare.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 7.* FAILURE$
diff --git a/regression/strings/java_concat/test.desc b/regression/strings/java_concat/test.desc
index 2dcca464779..6063f361aa5 100644
--- a/regression/strings/java_concat/test.desc
+++ b/regression/strings/java_concat/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_concat.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 10.* SUCCESS$
diff --git a/regression/strings/java_contains/test.desc b/regression/strings/java_contains/test.desc
index e5bb1edbc3b..c5166216bb1 100644
--- a/regression/strings/java_contains/test.desc
+++ b/regression/strings/java_contains/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_contains.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 7.* FAILURE$
diff --git a/regression/strings/java_delete/test.desc b/regression/strings/java_delete/test.desc
index 964669b6896..721165e152d 100644
--- a/regression/strings/java_delete/test.desc
+++ b/regression/strings/java_delete/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/regression/strings/java_delete_char_at/test.desc b/regression/strings/java_delete_char_at/test.desc
index 8450851614c..2ec7b55da93 100644
--- a/regression/strings/java_delete_char_at/test.desc
+++ b/regression/strings/java_delete_char_at/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_delete_char_at.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 9.* FAILURE$
diff --git a/regression/strings/java_easychair/test.desc b/regression/strings/java_easychair/test.desc
index 004b61e2b18..079e02ddee2 100644
--- a/regression/strings/java_easychair/test.desc
+++ b/regression/strings/java_easychair/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 easychair.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 30.* FAILURE$
diff --git a/regression/strings/java_empty/test.desc b/regression/strings/java_empty/test.desc
index 0d2635c6963..4c9cf9d82eb 100644
--- a/regression/strings/java_empty/test.desc
+++ b/regression/strings/java_empty/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_empty.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 6.* FAILURE$
diff --git a/regression/strings/java_endswith/test.desc b/regression/strings/java_endswith/test.desc
index 8d6444b75bd..10f8a8b0e2f 100644
--- a/regression/strings/java_endswith/test.desc
+++ b/regression/strings/java_endswith/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_endswith.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 7.* FAILURE$
diff --git a/regression/strings/java_equal/test.desc b/regression/strings/java_equal/test.desc
index 3e744a2eb05..bd4d1022d78 100644
--- a/regression/strings/java_equal/test.desc
+++ b/regression/strings/java_equal/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_equal.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/regression/strings/java_float/test.desc b/regression/strings/java_float/test.desc
index 7a560bf3ccf..d79c25dab3a 100644
--- a/regression/strings/java_float/test.desc
+++ b/regression/strings/java_float/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 test_float.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 15.* FAILURE$
diff --git a/regression/strings/java_hash_code/test.desc b/regression/strings/java_hash_code/test.desc
index b8893f4a9b0..70dfc7e6bbe 100644
--- a/regression/strings/java_hash_code/test.desc
+++ b/regression/strings/java_hash_code/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_hash_code.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 7.* FAILURE$
diff --git a/regression/strings/java_index_of/test.desc b/regression/strings/java_index_of/test.desc
index 67ff3297142..b4289558902 100644
--- a/regression/strings/java_index_of/test.desc
+++ b/regression/strings/java_index_of/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/regression/strings/java_index_of_char/test.desc b/regression/strings/java_index_of_char/test.desc
index 83fbccc0515..e40554cc835 100644
--- a/regression/strings/java_index_of_char/test.desc
+++ b/regression/strings/java_index_of_char/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_index_of_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$
diff --git a/regression/strings/java_insert_multiple/test.desc b/regression/strings/java_insert_multiple/test.desc
index 3ad6df9d1e2..cae43d53985 100644
--- a/regression/strings/java_insert_multiple/test.desc
+++ b/regression/strings/java_insert_multiple/test.desc
@@ -1,6 +1,6 @@
 CORE
 test_insert_multiple.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 9.* FAILURE$
diff --git a/regression/strings/test1/test.desc b/regression/strings/test1/test.desc
index 2e0b38c3ae3..7fdf7649b86 100644
--- a/regression/strings/test1/test.desc
+++ b/regression/strings/test1/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion c1 == c2: SUCCESS$
diff --git a/regression/strings/test2/test.desc b/regression/strings/test2/test.desc
index 809cbcdaa29..c3457da325a 100644
--- a/regression/strings/test2/test.desc
+++ b/regression/strings/test2/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion n == 5: SUCCESS$
diff --git a/regression/strings/test3.1/test.desc b/regression/strings/test3.1/test.desc
index 6fddff4c129..28b09f80cbb 100644
--- a/regression/strings/test3.1/test.desc
+++ b/regression/strings/test3.1/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.2/test.desc b/regression/strings/test3.2/test.desc
index 6fddff4c129..28b09f80cbb 100644
--- a/regression/strings/test3.2/test.desc
+++ b/regression/strings/test3.2/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.3/test.desc b/regression/strings/test3.3/test.desc
index 6fddff4c129..28b09f80cbb 100644
--- a/regression/strings/test3.3/test.desc
+++ b/regression/strings/test3.3/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3.4/test.desc b/regression/strings/test3.4/test.desc
index fc1cde2392c..87e4f8c97ae 100644
--- a/regression/strings/test3.4/test.desc
+++ b/regression/strings/test3.4/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test_init.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test3/test.desc b/regression/strings/test3/test.desc
index f6f9a63520a..20e7e66c522 100644
--- a/regression/strings/test3/test.desc
+++ b/regression/strings/test3/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_string_length\(s\) == i \+ 5: SUCCESS$
diff --git a/regression/strings/test4/test.desc b/regression/strings/test4/test.desc
index 6fddff4c129..28b09f80cbb 100644
--- a/regression/strings/test4/test.desc
+++ b/regression/strings/test4/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/strings/test5/test.desc b/regression/strings/test5/test.desc
index 303defd9de4..cc9ce200da3 100644
--- a/regression/strings/test5/test.desc
+++ b/regression/strings/test5/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/strings/test_char_set/test.desc b/regression/strings/test_char_set/test.desc
index 360759faf98..1266bbac4d5 100644
--- a/regression/strings/test_char_set/test.desc
+++ b/regression/strings/test_char_set/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* SUCCESS$
diff --git a/regression/strings/test_concat/test.desc b/regression/strings/test_concat/test.desc
index 317a4d1b4dd..c2ff491673f 100644
--- a/regression/strings/test_concat/test.desc
+++ b/regression/strings/test_concat/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion c == .p.: SUCCESS$
diff --git a/regression/strings/test_contains/test.desc b/regression/strings/test_contains/test.desc
index b0e33ce2b43..44862a304a8 100644
--- a/regression/strings/test_contains/test.desc
+++ b/regression/strings/test_contains/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion !__CPROVER_uninterpreted_string_contains_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"3\"\)): SUCCESS$
diff --git a/regression/strings/test_equal/test.desc b/regression/strings/test_equal/test.desc
index 34297ec50f5..7647a04397f 100644
--- a/regression/strings/test_equal/test.desc
+++ b/regression/strings/test_equal/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*.assertion.1\].* SUCCESS$
diff --git a/regression/strings/test_index_of/test.desc b/regression/strings/test_index_of/test.desc
index a2c12c3d259..dcb245dbf5e 100644
--- a/regression/strings/test_index_of/test.desc
+++ b/regression/strings/test_index_of/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion firstSlash == 3: SUCCESS$
diff --git a/regression/strings/test_int/test.desc b/regression/strings/test_int/test.desc
index fcce43ca76c..0638394661c 100644
--- a/regression/strings/test_int/test.desc
+++ b/regression/strings/test_int/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_char_at\(s,0\) == .1.: SUCCESS$
diff --git a/regression/strings/test_pass1/test.desc b/regression/strings/test_pass1/test.desc
index f2f54e69921..77f0c2e7eb8 100644
--- a/regression/strings/test_pass1/test.desc
+++ b/regression/strings/test_pass1/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_uninterpreted_string_equal_func\(t, __CPROVER_uninterpreted_string_literal_func\(\"a\"\)): SUCCESS
diff --git a/regression/strings/test_pass_pc3/test.desc b/regression/strings/test_pass_pc3/test.desc
index f1f3d1618c8..a88fd61db47 100644
--- a/regression/strings/test_pass_pc3/test.desc
+++ b/regression/strings/test_pass_pc3/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_string_length\(s3\) == 0: FAILURE$
diff --git a/regression/strings/test_prefix/test.desc b/regression/strings/test_prefix/test.desc
index be0ed5dc69e..53e37ec7dc8 100644
--- a/regression/strings/test_prefix/test.desc
+++ b/regression/strings/test_prefix/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion b: SUCCESS$
diff --git a/regression/strings/test_strlen/test.desc b/regression/strings/test_strlen/test.desc
index 28ed1b7e698..9040a64de73 100644
--- a/regression/strings/test_strlen/test.desc
+++ b/regression/strings/test_strlen/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion len_s == len_t: SUCCESS$
diff --git a/regression/strings/test_substring/test.desc b/regression/strings/test_substring/test.desc
index f0e4b5832b2..cbde7978b4c 100644
--- a/regression/strings/test_substring/test.desc
+++ b/regression/strings/test_substring/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* SUCCESS$
diff --git a/regression/strings/test_suffix/test.desc b/regression/strings/test_suffix/test.desc
index e7e8c1e36be..e9c8580be6f 100644
--- a/regression/strings/test_suffix/test.desc
+++ b/regression/strings/test_suffix/test.desc
@@ -1,6 +1,6 @@
 FUTURE
 test.c
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.1\] assertion __CPROVER_string_issuffix\(__CPROVER_string_literal\("po"\),s\): SUCCESS$
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 8e7947d9636..5ccfecaf81c 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/src/java_bytecode/java_string_library_preprocess.cpp
@@ -287,32 +287,27 @@ exprt::operandst java_string_library_preprocesst::process_parameters(
   return process_operands(ops, loc, symbol_table, init_code);
 }
 
-/// Creates a string_exprt from the input exprt and adds it to processed_ops
-/// \param processed_ops: the list of processed operands to populate
-/// \param op_to_process: a list of expressions
+/// Creates a string_exprt from the input exprt representing a char sequence
+/// \param expr_to_process: an expression of a type which implements char
+///        sequence
 /// \param loc: location in the source
 /// \param symbol_table: symbol table
 /// \param init_code: code block, in which declaration of some arguments may be
 ///   added
-void java_string_library_preprocesst::process_single_operand(
-  exprt::operandst &processed_ops,
-  const exprt &op_to_process,
+/// \return the processed operand
+exprt java_string_library_preprocesst::convert_exprt_to_string_exprt(
+  const exprt &expr_to_process,
   const source_locationt &loc,
   symbol_tablet &symbol_table,
   code_blockt &init_code)
 {
-  member_exprt length(
-    op_to_process, "length", string_length_type());
-  member_exprt data(op_to_process, "data", string_data_type(symbol_table));
-  dereference_exprt deref_data(data, data.type().subtype());
+  PRECONDITION(implements_java_char_sequence(expr_to_process.type()));
   string_exprt string_expr=fresh_string_expr(loc, symbol_table, init_code);
+  code_assign_java_string_to_string_expr(
+    string_expr, expr_to_process, symbol_table, init_code);
   exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, init_code);
-  init_code.add(code_declt(string_expr_sym));
-  init_code.add(code_assignt(string_expr.length(), length));
-  init_code.add(
-    code_assignt(string_expr.content(), deref_data));
   init_code.add(code_assignt(string_expr_sym, string_expr));
-  processed_ops.push_back(string_expr);
+  return string_expr;
 }
 
 /// for each expression that is of a type implementing strings, we declare a new
@@ -336,19 +331,12 @@ exprt::operandst java_string_library_preprocesst::process_operands(
   for(const auto &p : operands)
   {
     if(implements_java_char_sequence(p.type()))
-    {
-      dereference_exprt deref=
-        checked_dereference(p, to_pointer_type(p.type()).subtype());
-      process_single_operand(ops, deref, loc, symbol_table, init_code);
-    }
+      ops.push_back(
+        convert_exprt_to_string_exprt(p, loc, symbol_table, init_code));
     else if(is_java_char_array_pointer_type(p.type()))
-    {
       ops.push_back(replace_char_array(p, loc, symbol_table, init_code));
-    }
     else
-    {
       ops.push_back(p);
-    }
   }
   return ops;
 }
@@ -370,22 +358,19 @@ exprt::operandst
   code_blockt &init_code)
 {
   PRECONDITION(operands.size()==2);
-  exprt::operandst ops;
   const exprt &op0=operands[0];
-  const exprt &op1=operands[1];
   PRECONDITION(implements_java_char_sequence(op0.type()));
 
-  dereference_exprt deref0=
-    checked_dereference(op0, to_pointer_type(op0.type()).subtype());
-  process_single_operand(ops, deref0, loc, symbol_table, init_code);
+  exprt::operandst ops;
+  ops.push_back(
+    convert_exprt_to_string_exprt(op0, loc, symbol_table, init_code));
 
   // TODO: Manage the case where we have a non-String Object (this should
   // probably be handled upstream. At any rate, the following code should be
   // protected with assertions on the type of op1.
-  typecast_exprt tcast(op1, to_pointer_type(op0.type()));
-  dereference_exprt deref1=
-    checked_dereference(tcast, to_pointer_type(op0.type()).subtype());
-  process_single_operand(ops, deref1, loc, symbol_table, init_code);
+  typecast_exprt tcast(operands[1], to_pointer_type(op0.type()));
+  ops.push_back(
+    convert_exprt_to_string_exprt(tcast, loc, symbol_table, init_code));
   return ops;
 }
 
@@ -796,13 +781,16 @@ codet java_string_library_preprocesst::
 /// \param lhs: a string expression
 /// \param rhs: an expression representing a java string
 /// \param symbol_table: symbol table
-/// \return return the following code:
+/// \param code: code block that gets appended the following code:
 /// ~~~~~~~~~~~~~~~~~~~~~~
 /// lhs.length=rhs->length
 /// lhs.data=*(rhs->data)
 /// ~~~~~~~~~~~~~~~~~~~~~~
-codet java_string_library_preprocesst::code_assign_java_string_to_string_expr(
-  const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table)
+void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
+  const string_exprt &lhs,
+  const exprt &rhs,
+  symbol_tablet &symbol_table,
+  code_blockt &code)
 {
   PRECONDITION(implements_java_char_sequence(rhs.type()));
 
@@ -821,7 +809,6 @@ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr(
   dereference_exprt rhs_data(member_data, member_data.type().subtype());
 
   // Assignments
-  code_blockt code;
   code.add(code_assignt(lhs.length(), rhs_length));
 
   // We always assume data of a String is not null
@@ -829,7 +816,6 @@ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr(
     member_data, null_pointer_exprt(to_pointer_type(member_data.type()))));
   code.add(code_assumet(data_not_null));
   code.add(code_assignt(lhs.content(), rhs_data));
-  return code;
 }
 
 /// \param lhs: an expression representing a java string
@@ -1155,8 +1141,8 @@ codet java_string_library_preprocesst::make_string_to_char_array_code(
 
   // string_expr = {this->length, this->data}
   string_exprt string_expr=fresh_string_expr(loc, symbol_table, code);
-  code.add(code_assign_java_string_to_string_expr(
-    string_expr, string_argument, symbol_table));
+  code_assign_java_string_to_string_expr(
+    string_expr, string_argument, symbol_table, code);
   exprt string_expr_sym=fresh_string_expr_symbol(
     loc, symbol_table, code);
   code.add(code_assignt(string_expr_sym, string_expr));
@@ -1406,8 +1392,11 @@ exprt java_string_library_preprocesst::make_argument_for_format(
       pointer_typet string_pointer=
         java_reference_type(symbol_typet("java::java.lang.String"));
       typecast_exprt arg_i_as_string(arg_i, string_pointer);
-      code_not_null.add(code_assign_java_string_to_string_expr(
-        to_string_expr(field_expr), arg_i_as_string, symbol_table));
+      code_assign_java_string_to_string_expr(
+        to_string_expr(field_expr),
+        arg_i_as_string,
+        symbol_table,
+        code_not_null);
       exprt arg_i_string_expr_sym=fresh_string_expr_symbol(
         loc, symbol_table, code_not_null);
       code_not_null.add(code_assignt(
@@ -1666,8 +1655,7 @@ codet java_string_library_preprocesst::make_copy_string_code(
   // Assign the argument to string_expr
   code_typet::parametert op=type.parameters()[0];
   symbol_exprt arg0(op.get_identifier(), op.type());
-  code.add(code_assign_java_string_to_string_expr(
-    string_expr, arg0, symbol_table));
+  code_assign_java_string_to_string_expr(string_expr, arg0, symbol_table, code);
 
   // Assign string_expr to string_expr_sym
   exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code);
@@ -1708,8 +1696,7 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
   // Assign argument to a string_expr
   code_typet::parameterst params=type.parameters();
   symbol_exprt arg1(params[1].get_identifier(), params[1].type());
-  code.add(code_assign_java_string_to_string_expr(
-    string_expr, arg1, symbol_table));
+  code_assign_java_string_to_string_expr(string_expr, arg1, symbol_table, code);
 
   // Assign string_expr to symbol to keep track of it
   exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code);
@@ -1750,8 +1737,8 @@ codet java_string_library_preprocesst::make_string_length_code(
   string_exprt str_expr=fresh_string_expr(loc, symbol_table, code);
 
   // Assign this to str_expr
-  code.add(
-    code_assign_java_string_to_string_expr(str_expr, arg_this, symbol_table));
+  code_assign_java_string_to_string_expr(
+    str_expr, arg_this, symbol_table, code);
 
   // Assign str_expr to str_expr_sym for that expression to be present in the
   // symbol table in order to be processed by the string solver
diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h
index cc8dd4cf469..cff80bea63f 100644
--- a/src/java_bytecode/java_string_library_preprocess.h
+++ b/src/java_bytecode/java_string_library_preprocess.h
@@ -173,8 +173,14 @@ class java_string_library_preprocesst:public messaget
     symbol_tablet &symbol_table,
     code_blockt &init_code);
 
-  void process_single_operand(
-    exprt::operandst &processed_ops,
+  friend exprt convert_exprt_to_string_exprt_unit_test(
+      java_string_library_preprocesst &preprocess,
+      const exprt &deref,
+      const source_locationt &loc,
+      symbol_tablet &symbol_table,
+      code_blockt &init_code);
+
+  exprt convert_exprt_to_string_exprt(
     const exprt &deref,
     const source_locationt &loc,
     symbol_tablet &symbol_table,
@@ -286,8 +292,11 @@ class java_string_library_preprocesst:public messaget
     const source_locationt &loc,
     symbol_tablet &symbol_table);
 
-  codet code_assign_java_string_to_string_expr(
-    const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table);
+  void code_assign_java_string_to_string_expr(
+    const string_exprt &lhs,
+    const exprt &rhs,
+    symbol_tablet &symbol_table,
+    code_blockt &code);
 
   codet code_assign_string_literal_to_string_expr(
     const string_exprt &lhs,
diff --git a/unit/Makefile b/unit/Makefile
index 0f81813e67e..a9f4da75522 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -20,6 +20,7 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
        miniBDD_new.cpp \
+       java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
new file mode 100644
index 00000000000..f7125f4fe17
--- /dev/null
+++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
@@ -0,0 +1,59 @@
+/*******************************************************************\
+
+ Module: Java string library preprocess.
+         Test for converting an expression to a string expression.
+
+ Author: Diffblue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <catch.hpp>
+#include <util/c_types.h>
+#include <util/expr.h>
+#include <util/std_code.h>
+#include <java_bytecode/java_string_library_preprocess.h>
+#include <langapi/language_util.h>
+#include <java_bytecode/java_bytecode_language.h>
+#include <util/namespace.h>
+#include <langapi/mode.h>
+
+exprt convert_exprt_to_string_exprt_unit_test(
+  java_string_library_preprocesst &preprocess,
+  const exprt &deref,
+  const source_locationt &loc,
+  symbol_tablet &symbol_table,
+  code_blockt &init_code)
+{
+  return preprocess.convert_exprt_to_string_exprt(
+    deref, loc, symbol_table, init_code);
+}
+
+TEST_CASE("Convert exprt to string exprt")
+{
+  source_locationt loc;
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+  code_blockt code;
+  java_string_library_preprocesst preprocess;
+  preprocess.add_string_type("java.lang.String", symbol_table);
+  symbol_typet java_string_type("java::java.lang.String");
+  symbol_exprt expr("a", pointer_type(java_string_type));
+  convert_exprt_to_string_exprt_unit_test(
+    preprocess, expr, loc, symbol_table, code);
+  register_language(new_java_bytecode_language);
+
+  std::vector<std::string> code_string;
+  for(auto op : code.operands())
+    code_string.push_back(from_expr(ns, "", op));
+
+  REQUIRE(code_string.size()==7);
+  REQUIRE(code_string[0]=="int cprover_string_length$1;");
+  REQUIRE(code_string[1]=="char cprover_string_array$2[INFINITY()];");
+  REQUIRE(code_string[2]=="cprover_string_length$1 = a->length;");
+  REQUIRE(code_string[3]=="__CPROVER_assume(!(a->data == null));");
+  REQUIRE(code_string[4]=="cprover_string_array$2 = *a->data;");
+  REQUIRE(code_string[5]=="struct __CPROVER_refined_string_type { int length; "
+    "char content[INFINITY()]; } cprover_string$3;");
+  REQUIRE(code_string[6]=="cprover_string$3 = { .=cprover_string_length$1, "
+    ".=cprover_string_array$2 };");
+}