From 21eeb297950fc06e830c293e015e0302fa590bbe Mon Sep 17 00:00:00 2001 From: Joel Allred Date: Thu, 20 Apr 2017 09:46:20 +0100 Subject: [PATCH 1/2] Enable working smoke tests Set the currently working some tests as CORE and link the others to GitHub issues. --- regression/strings-smoke-tests/java_append_char/test.desc | 2 +- regression/strings-smoke-tests/java_append_int/test.desc | 2 +- regression/strings-smoke-tests/java_append_object/test.desc | 1 + regression/strings-smoke-tests/java_append_string/test.desc | 2 +- regression/strings-smoke-tests/java_case/test.desc | 2 +- regression/strings-smoke-tests/java_char_array/test.desc | 2 +- regression/strings-smoke-tests/java_char_array_init/test.desc | 1 + regression/strings-smoke-tests/java_char_at/test.desc | 2 +- regression/strings-smoke-tests/java_code_point/test.desc | 2 +- regression/strings-smoke-tests/java_compare/test.desc | 2 +- regression/strings-smoke-tests/java_concat/test.desc | 2 +- regression/strings-smoke-tests/java_contains/test.desc | 3 ++- regression/strings-smoke-tests/java_delete/test.desc | 2 +- regression/strings-smoke-tests/java_delete_char_at/test.desc | 2 +- regression/strings-smoke-tests/java_empty/test.desc | 2 +- regression/strings-smoke-tests/java_endswith/test.desc | 2 +- regression/strings-smoke-tests/java_equal/test.desc | 4 ++-- regression/strings-smoke-tests/java_float/test.desc | 2 +- regression/strings-smoke-tests/java_hash_code/test.desc | 2 +- regression/strings-smoke-tests/java_index_of/test.desc | 3 ++- regression/strings-smoke-tests/java_index_of_char/test.desc | 3 ++- regression/strings-smoke-tests/java_insert_char/test.desc | 2 +- .../strings-smoke-tests/java_insert_char_array/test.desc | 2 +- regression/strings-smoke-tests/java_insert_int/test.desc | 2 +- regression/strings-smoke-tests/java_insert_multiple/test.desc | 2 +- regression/strings-smoke-tests/java_insert_string/test.desc | 2 +- regression/strings-smoke-tests/java_int_to_string/test.desc | 2 +- regression/strings-smoke-tests/java_intern/test.desc | 2 +- regression/strings-smoke-tests/java_last_index_of/test.desc | 3 ++- .../strings-smoke-tests/java_last_index_of_char/test.desc | 2 +- regression/strings-smoke-tests/java_length/test.desc | 2 +- regression/strings-smoke-tests/java_parseint/test.desc | 2 +- regression/strings-smoke-tests/java_replace/test.desc | 3 ++- regression/strings-smoke-tests/java_replace_char/test.desc | 2 +- regression/strings-smoke-tests/java_set_char_at/test.desc | 2 +- regression/strings-smoke-tests/java_set_length/test.desc | 4 ++-- regression/strings-smoke-tests/java_starts_with/test.desc | 2 +- .../strings-smoke-tests/java_string_builder_length/test.desc | 2 +- regression/strings-smoke-tests/java_subsequence/test.desc | 2 +- regression/strings-smoke-tests/java_substring/test.desc | 2 +- regression/strings-smoke-tests/java_trim/test.desc | 4 ++-- 41 files changed, 49 insertions(+), 42 deletions(-) diff --git a/regression/strings-smoke-tests/java_append_char/test.desc b/regression/strings-smoke-tests/java_append_char/test.desc index 0f1b3ae243f..88d1cbf2114 100644 --- a/regression/strings-smoke-tests/java_append_char/test.desc +++ b/regression/strings-smoke-tests/java_append_char/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_append_char.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_append_int/test.desc b/regression/strings-smoke-tests/java_append_int/test.desc index e1455859470..e0b30e7827d 100644 --- a/regression/strings-smoke-tests/java_append_int/test.desc +++ b/regression/strings-smoke-tests/java_append_int/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_append_int.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_append_object/test.desc b/regression/strings-smoke-tests/java_append_object/test.desc index 5db2ac1db73..787852963ed 100644 --- a/regression/strings-smoke-tests/java_append_object/test.desc +++ b/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 diff --git a/regression/strings-smoke-tests/java_append_string/test.desc b/regression/strings-smoke-tests/java_append_string/test.desc index 18035539d58..943ca820bcc 100644 --- a/regression/strings-smoke-tests/java_append_string/test.desc +++ b/regression/strings-smoke-tests/java_append_string/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_append_string.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_case/test.desc b/regression/strings-smoke-tests/java_case/test.desc index e01a5054419..9a254ae3484 100644 --- a/regression/strings-smoke-tests/java_case/test.desc +++ b/regression/strings-smoke-tests/java_case/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_case.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_char_array/test.desc b/regression/strings-smoke-tests/java_char_array/test.desc index ecce56c1ab8..efb6ad4c5d7 100644 --- a/regression/strings-smoke-tests/java_char_array/test.desc +++ b/regression/strings-smoke-tests/java_char_array/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_char_array.class --refine-strings ^EXIT=0$ 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 fc1cde2392c..04096a8a984 100644 --- a/regression/strings-smoke-tests/java_char_array_init/test.desc +++ b/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 diff --git a/regression/strings-smoke-tests/java_char_at/test.desc b/regression/strings-smoke-tests/java_char_at/test.desc index 5bf29fc7a4d..f2d5ecad6c7 100644 --- a/regression/strings-smoke-tests/java_char_at/test.desc +++ b/regression/strings-smoke-tests/java_char_at/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_char_at.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_code_point/test.desc b/regression/strings-smoke-tests/java_code_point/test.desc index 012c7c3501b..e3be9616fa5 100644 --- a/regression/strings-smoke-tests/java_code_point/test.desc +++ b/regression/strings-smoke-tests/java_code_point/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_code_point.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_compare/test.desc b/regression/strings-smoke-tests/java_compare/test.desc index 38aa025f416..9e6810476b9 100644 --- a/regression/strings-smoke-tests/java_compare/test.desc +++ b/regression/strings-smoke-tests/java_compare/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_compare.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_concat/test.desc b/regression/strings-smoke-tests/java_concat/test.desc index fb784efd723..2dcca464779 100644 --- a/regression/strings-smoke-tests/java_concat/test.desc +++ b/regression/strings-smoke-tests/java_concat/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_concat.class --refine-strings ^EXIT=10$ diff --git a/regression/strings-smoke-tests/java_contains/test.desc b/regression/strings-smoke-tests/java_contains/test.desc index 2b96346d718..e40d51aa473 100644 --- a/regression/strings-smoke-tests/java_contains/test.desc +++ b/regression/strings-smoke-tests/java_contains/test.desc @@ -1,4 +1,4 @@ -FUTURE +KNOWNBUG test_contains.class --refine-strings ^EXIT=10$ @@ -6,3 +6,4 @@ test_contains.class ^\[.*assertion.1\].* line 8.* SUCCESS$ ^\[.*assertion.2\].* line 9.* FAILURE$ -- +Issue: diffblue/test-gen#201 diff --git a/regression/strings-smoke-tests/java_delete/test.desc b/regression/strings-smoke-tests/java_delete/test.desc index 27a1406cdb7..f0c0aedda91 100644 --- a/regression/strings-smoke-tests/java_delete/test.desc +++ b/regression/strings-smoke-tests/java_delete/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_delete.class --refine-strings ^EXIT=0$ 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 94ba56a2c54..d415d16e9b6 100644 --- a/regression/strings-smoke-tests/java_delete_char_at/test.desc +++ b/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$ diff --git a/regression/strings-smoke-tests/java_empty/test.desc b/regression/strings-smoke-tests/java_empty/test.desc index 9951c8a13ee..181ff4ee5fd 100644 --- a/regression/strings-smoke-tests/java_empty/test.desc +++ b/regression/strings-smoke-tests/java_empty/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_empty.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_endswith/test.desc b/regression/strings-smoke-tests/java_endswith/test.desc index 0461a3e50e6..8b058f48d78 100644 --- a/regression/strings-smoke-tests/java_endswith/test.desc +++ b/regression/strings-smoke-tests/java_endswith/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_endswith.class --refine-strings ^EXIT=10$ diff --git a/regression/strings-smoke-tests/java_equal/test.desc b/regression/strings-smoke-tests/java_equal/test.desc index 05f0f383230..964c3b72bae 100644 --- a/regression/strings-smoke-tests/java_equal/test.desc +++ b/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$ diff --git a/regression/strings-smoke-tests/java_float/test.desc b/regression/strings-smoke-tests/java_float/test.desc index 427d1fca836..e81b6b4feba 100644 --- a/regression/strings-smoke-tests/java_float/test.desc +++ b/regression/strings-smoke-tests/java_float/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_float.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_hash_code/test.desc b/regression/strings-smoke-tests/java_hash_code/test.desc index 2db8d7116f9..fc628393186 100644 --- a/regression/strings-smoke-tests/java_hash_code/test.desc +++ b/regression/strings-smoke-tests/java_hash_code/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_hash_code.class --refine-strings ^EXIT=10$ diff --git a/regression/strings-smoke-tests/java_index_of/test.desc b/regression/strings-smoke-tests/java_index_of/test.desc index f2fa825597d..6033af25d1b 100644 --- a/regression/strings-smoke-tests/java_index_of/test.desc +++ b/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 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 63382a455f3..a95467b52e4 100644 --- a/regression/strings-smoke-tests/java_index_of_char/test.desc +++ b/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 diff --git a/regression/strings-smoke-tests/java_insert_char/test.desc b/regression/strings-smoke-tests/java_insert_char/test.desc index 77d3ce2ebd9..0e9a06d5afb 100644 --- a/regression/strings-smoke-tests/java_insert_char/test.desc +++ b/regression/strings-smoke-tests/java_insert_char/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_char.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_insert_char_array/test.desc b/regression/strings-smoke-tests/java_insert_char_array/test.desc index d48c601b61b..082771dd2db 100644 --- a/regression/strings-smoke-tests/java_insert_char_array/test.desc +++ b/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$ diff --git a/regression/strings-smoke-tests/java_insert_int/test.desc b/regression/strings-smoke-tests/java_insert_int/test.desc index dc039fedbea..df87a5f5728 100644 --- a/regression/strings-smoke-tests/java_insert_int/test.desc +++ b/regression/strings-smoke-tests/java_insert_int/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_int.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_insert_multiple/test.desc b/regression/strings-smoke-tests/java_insert_multiple/test.desc index 983d416dd3b..bb9a23f1b5c 100644 --- a/regression/strings-smoke-tests/java_insert_multiple/test.desc +++ b/regression/strings-smoke-tests/java_insert_multiple/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_multiple.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_insert_string/test.desc b/regression/strings-smoke-tests/java_insert_string/test.desc index b438d32d6d9..44bf9f268d9 100644 --- a/regression/strings-smoke-tests/java_insert_string/test.desc +++ b/regression/strings-smoke-tests/java_insert_string/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_insert_string.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_int_to_string/test.desc b/regression/strings-smoke-tests/java_int_to_string/test.desc index a615a10f538..38fa5289bd2 100644 --- a/regression/strings-smoke-tests/java_int_to_string/test.desc +++ b/regression/strings-smoke-tests/java_int_to_string/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_int.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_intern/test.desc b/regression/strings-smoke-tests/java_intern/test.desc index 645e267029c..c8d0eea43bd 100644 --- a/regression/strings-smoke-tests/java_intern/test.desc +++ b/regression/strings-smoke-tests/java_intern/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_intern.class --refine-strings ^EXIT=0$ 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 77bc5b7f18f..5ee1604e846 100644 --- a/regression/strings-smoke-tests/java_last_index_of/test.desc +++ b/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 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 3e9a3d4b547..aa88fc5f6ef 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,4 +1,4 @@ -FUTURE +CORE test_last_index_of_char.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_length/test.desc b/regression/strings-smoke-tests/java_length/test.desc index 913afbf13c7..d7f0e02feca 100644 --- a/regression/strings-smoke-tests/java_length/test.desc +++ b/regression/strings-smoke-tests/java_length/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_length.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_parseint/test.desc b/regression/strings-smoke-tests/java_parseint/test.desc index 9cb70f5a957..6a513e61deb 100644 --- a/regression/strings-smoke-tests/java_parseint/test.desc +++ b/regression/strings-smoke-tests/java_parseint/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_parseint.class --refine-strings ^EXIT=10$ diff --git a/regression/strings-smoke-tests/java_replace/test.desc b/regression/strings-smoke-tests/java_replace/test.desc index 59c7d326a0b..d86aae6b5a9 100644 --- a/regression/strings-smoke-tests/java_replace/test.desc +++ b/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 diff --git a/regression/strings-smoke-tests/java_replace_char/test.desc b/regression/strings-smoke-tests/java_replace_char/test.desc index 528d4eead6c..5c336326e5d 100644 --- a/regression/strings-smoke-tests/java_replace_char/test.desc +++ b/regression/strings-smoke-tests/java_replace_char/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_replace_char.class --refine-strings ^EXIT=0$ 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 650e7712278..1c471d0194a 100644 --- a/regression/strings-smoke-tests/java_set_char_at/test.desc +++ b/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$ diff --git a/regression/strings-smoke-tests/java_set_length/test.desc b/regression/strings-smoke-tests/java_set_length/test.desc index ab59e459eb1..d19eb265fa4 100644 --- a/regression/strings-smoke-tests/java_set_length/test.desc +++ b/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$ diff --git a/regression/strings-smoke-tests/java_starts_with/test.desc b/regression/strings-smoke-tests/java_starts_with/test.desc index 5c5d85565c2..ec6b84102f2 100644 --- a/regression/strings-smoke-tests/java_starts_with/test.desc +++ b/regression/strings-smoke-tests/java_starts_with/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_starts_with.class --refine-strings ^EXIT=10$ 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 ba9187109ed..2a37e02a36c 100644 --- a/regression/strings-smoke-tests/java_string_builder_length/test.desc +++ b/regression/strings-smoke-tests/java_string_builder_length/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_sb_length.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_subsequence/test.desc b/regression/strings-smoke-tests/java_subsequence/test.desc index 34585a7900d..df3cc28619f 100644 --- a/regression/strings-smoke-tests/java_subsequence/test.desc +++ b/regression/strings-smoke-tests/java_subsequence/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_subsequence.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_substring/test.desc b/regression/strings-smoke-tests/java_substring/test.desc index 8a29460f529..26ec800cfac 100644 --- a/regression/strings-smoke-tests/java_substring/test.desc +++ b/regression/strings-smoke-tests/java_substring/test.desc @@ -1,4 +1,4 @@ -FUTURE +CORE test_substring.class --refine-strings ^EXIT=0$ diff --git a/regression/strings-smoke-tests/java_trim/test.desc b/regression/strings-smoke-tests/java_trim/test.desc index c7a307c37ed..171ada28356 100644 --- a/regression/strings-smoke-tests/java_trim/test.desc +++ b/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$ From 95844654fcfb0e7754a77e789eeb4ef9b9780fff Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 13 Apr 2017 15:55:07 +0100 Subject: [PATCH 2/2] Correction in add_axioms_for_set_length This corrects issue diffblue/test-gen#244 There was a an error in add_axioms_for_set_length: |s1| was compared to idx instead of comparing k to idx. The second assertion was splitted into two to make constraints clearer. Applied changes requested by Matthias --- ...ng_constraint_generator_transformation.cpp | 23 ++++++++++++------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index f27fe5d4317..c110f636c43 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/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 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; }