diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 1102011302a..d9d69abf325 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -181,7 +181,7 @@ class string_constraint_generatort final static constant_exprt constant_char(int i, const typet &char_type); - array_string_exprt + const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length); exprt axiom_for_is_positive_index(const exprt &x); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index db60ef1e786..41f7cf193d7 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -389,13 +389,11 @@ array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length) /// Adds creates a new array if it does not already exists /// \todo This should be replaced /// by array_poolt.make_char_array_for_char_pointer -array_string_exprt string_constraint_generatort::char_array_of_pointer( +const array_string_exprt &string_constraint_generatort::char_array_of_pointer( const exprt &pointer, const exprt &length) { - const array_string_exprt array = array_pool.find(pointer, length); - created_strings.insert(array); - return array; + return *created_strings.insert(array_pool.find(pointer, length)).first; } array_string_exprt array_poolt::find(const refined_string_exprt &str)