Merge pull request diffblue#1241 from romainbrenguier/bugfix/check-axioms#874

Improvement in check_axioms method of the string solver

Author: Daniel Kroening

regression/strings-smoke-tests/java_append_char/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings-smoke-tests/java_case/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test_case.java line 10 .* SUCCESS$

regression/strings-smoke-tests/java_insert_char/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---refine-strings
+--refine-strings  --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings-smoke-tests/java_insert_char_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings-smoke-tests/java_insert_int/test.desc

@@ -1,6 +1,6 @@
 FUTURE
 test_insert_int.class
---refine-strings
+--refine-strings  --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings-smoke-tests/java_insert_multiple/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_multiple.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings-smoke-tests/java_insert_string/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_string.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/strings-smoke-tests/java_int_to_string/test3.desc

@@ -1,6 +1,6 @@
 CORE
 Test3.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/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_int_to_string_with_radix/test_binary1.desc

@@ -1,6 +1,6 @@
 CORE
 Test_binary1.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_binary2.desc

@@ -1,6 +1,6 @@
 CORE
 Test_binary2.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_hex1.desc

@@ -1,6 +1,6 @@
 CORE
 Test_hex1.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_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_int_to_string_with_radix/test_hex3.desc

@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

regression/strings-smoke-tests/java_int_to_string_with_radix/test_octal2.desc

@@ -1,6 +1,6 @@
 CORE
 Test_octal2.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_octal3.desc

@@ -1,6 +1,6 @@
 CORE
 Test_octal3.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_hex1.desc

@@ -1,6 +1,6 @@
 CORE
 Test_hex1.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_hex3.desc

@@ -1,6 +1,6 @@
 CORE
 Test_hex3.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal1.desc

@@ -1,6 +1,6 @@
 CORE
 Test_octal1.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal2.desc

@@ -1,6 +1,6 @@
 CORE
 Test_octal2.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

regression/strings-smoke-tests/java_long_to_string_with_radix/test_octal3.desc

@@ -1,6 +1,6 @@
 CORE
 Test_octal3.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* line 7 .* SUCCESS$

regression/strings-smoke-tests/java_value_of_float/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings --function test.check
+--refine-strings --function test.check --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 7 .* SUCCESS$

regression/strings-smoke-tests/java_value_of_float_2/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 test.class
---refine-strings --function test.check
+--refine-strings --function test.check --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 6 .* SUCCESS$

regression/strings-smoke-tests/java_value_of_long/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.* file test.java line 9 .* SUCCESS$

regression/strings/StringStartEnd02/test.desc

@@ -1,6 +1,6 @@
 CORE
 StringStartEnd02.class
---refine-strings --unwind 30
+--refine-strings --unwind 30 --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\] .* line 13 .* FAILURE$

regression/strings/java_append_char/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_append_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/strings/java_case/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_case.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$

regression/strings/java_char_array_init/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_init.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 14.* FAILURE$

regression/strings/java_insert_char/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_char.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$

regression/strings/java_insert_char_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_char_array.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 12.* FAILURE$

regression/strings/java_insert_int/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_int.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$

regression/strings/java_insert_string/test.desc

@@ -1,6 +1,6 @@
 CORE
 test_insert_string.class
---refine-strings
+--refine-strings --string-max-length 1000
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion\.1\].* line 8.* FAILURE$