diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 4efbfebc6a6..25ab5d7cd1f 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -2264,8 +2264,9 @@ exprt string_refinementt::get(const exprt &expr) const const exprt length = super_get(arr.length()); if(const auto n = numeric_cast(length)) { - const array_exprt arr_model(array_typet(arr.type().subtype(), length)); - return fill_in_array_expr(arr_model, generator.max_string_length); + const interval_sparse_arrayt sparse_array( + from_integer(CHARACTER_FOR_UNKNOWN, arr.type().subtype())); + return sparse_array.concretize(*n, length.type()); } } return arr; diff --git a/src/solvers/refinement/string_refinement_util.h b/src/solvers/refinement/string_refinement_util.h index d1ed9ae0710..d05c5a2d88c 100644 --- a/src/solvers/refinement/string_refinement_util.h +++ b/src/solvers/refinement/string_refinement_util.h @@ -148,7 +148,7 @@ class interval_sparse_arrayt final : public sparse_arrayt /// Complexity is linear in the number of entries. exprt at(std::size_t index) const override; -private: + /// Array containing the same value at each index. explicit interval_sparse_arrayt(exprt default_value) : sparse_arrayt(default_value) {