Refactoring assign_java_string_to_string_expr with process_operands

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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.

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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$

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

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$

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$

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$

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$