Skip to content

Commit 0803dac

Browse files
Refactor interval_sparse_array::concretize
1 parent 2de1298 commit 0803dac

File tree

1 file changed

+7
-8
lines changed

1 file changed

+7
-8
lines changed

src/solvers/refinement/string_refinement_util.cpp

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -209,16 +209,15 @@ array_exprt interval_sparse_arrayt::concretize(
209209
array_exprt array(array_type);
210210
array.operands().reserve(size);
211211

212-
std::size_t current_index = 0;
213-
for(const auto &pair : entries)
214-
{
215-
for(; current_index <= pair.first && current_index < size; ++current_index)
216-
array.operands().push_back(pair.second);
217-
}
218-
for(; current_index < size; ++current_index)
219-
array.operands().push_back(default_value);
212+
auto it = entries.begin();
213+
for(; it != entries.end() && it->first < size; ++it)
214+
array.operands().resize(it->first + 1, it->second);
215+
216+
array.operands().resize(
217+
size, it == entries.end() ? default_value : it->second);
220218
return array;
221219
}
220+
222221
void equation_symbol_mappingt::add(const std::size_t i, const exprt &expr)
223222
{
224223
equations_containing[expr].push_back(i);

0 commit comments

Comments
 (0)