Fix issue #244 - add_axioms_for_set_length

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_append_char.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_append_int.class
 --refine-strings
 ^EXIT=0$

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

@@ -5,3 +5,4 @@ test_append_object.class
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+Issue: diffblue/test-gen#82

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_append_string.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_case.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_char_array.class
 --refine-strings
 ^EXIT=0$

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

@@ -5,3 +5,4 @@ test_init.class
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+cbmc/test-gen#259

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_char_at.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_code_point.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_compare.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_concat.class
 --refine-strings
 ^EXIT=10$

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

@@ -1,8 +1,9 @@
-FUTURE
+KNOWNBUG
 test_contains.class
 --refine-strings
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$
 ^\[.*assertion.2\].* line 9.* FAILURE$
 --
+Issue: diffblue/test-gen#201

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_delete.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_delete_char_at.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_empty.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_endswith.class
 --refine-strings
 ^EXIT=10$

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

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

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_float.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_hash_code.class
 --refine-strings
 ^EXIT=10$

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

@@ -1,7 +1,8 @@
-FUTURE
+KNOWNBUG
 test_index_of.class
 --refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+Issue: cbmc/test-gen#77

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

@@ -1,7 +1,8 @@
-FUTURE
+CORE
 test_index_of_char.class
 --refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+Issue: cbmc/test-gen#77

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_char.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_char_array.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_int.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_multiple.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_insert_string.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_int.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_intern.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,7 +1,8 @@
-FUTURE
+KNOWNBUG
 test_last_index_of.class
 --refine-strings
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+Issue: diffblue/test-gen#77

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_last_index_of_char.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_length.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_parseint.class
 --refine-strings
 ^EXIT=10$

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

@@ -1,7 +1,8 @@
 FUTURE
 test_replace.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+diffblue/test-gen#256

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_replace_char.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_set_char_at.class
 --refine-strings
 ^EXIT=0$

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

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

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_starts_with.class
 --refine-strings
 ^EXIT=10$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_sb_length.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_subsequence.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,4 +1,4 @@
-FUTURE
+CORE
 test_substring.class
 --refine-strings
 ^EXIT=0$

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

@@ -1,6 +1,6 @@
-FUTURE
+CORE
 test_trim.class
---refine-strings
+--refine-strings --string-max-length 100
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* SUCCESS$

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -36,22 +36,29 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length(
 
   // We add axioms:
   // a1 : |res|=k
-  // a2 : forall i<k. (i<k ==> s[i]=s1[i]) &&(i >= k ==> s[i]=0)
+  // a2 : forall i<|s1|. i < |res|  ==> res[i] = s1[i]
+  // a3 : forall i<|s1|. i >= |res| ==> res[i] = 0
 
   axioms.push_back(res.axiom_for_has_length(k));
 
   symbol_exprt idx=fresh_univ_index(
     "QA_index_set_length", ref_type.get_index_type());
   string_constraintt a2(
-    idx, k, and_exprt(
-      implies_exprt(
-        s1.axiom_for_is_strictly_longer_than(idx),
-        equal_exprt(s1[idx], res[idx])),
-      implies_exprt(
-        s1.axiom_for_is_shorter_than(idx),
-        equal_exprt(s1[idx], constant_char(0, ref_type.get_char_type())))));
+    idx,
+    s1.length(),
+    res.axiom_for_is_strictly_longer_than(idx),
+    equal_exprt(s1[idx], res[idx]));
   axioms.push_back(a2);
 
+  symbol_exprt idx2=fresh_univ_index(
+    "QA_index_set_length2", ref_type.get_index_type());
+  string_constraintt a3(
+    idx2,
+    s1.length(),
+    res.axiom_for_is_shorter_than(idx2),
+    equal_exprt(res[idx2], constant_char(0, ref_type.get_char_type())));
+  axioms.push_back(a3);
+
   return res;
 }