Skip to content

Commit 234cdf8

Browse files
Correcting fill_in_vector function
We were using a mix of int and sizet that could cause compilation problems.
1 parent 059c2a2 commit 234cdf8

File tree

1 file changed

+10
-17
lines changed

1 file changed

+10
-17
lines changed

src/solvers/refinement/string_refinement.h

Lines changed: 10 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -170,24 +170,17 @@ exprt concretize_arrays_in_expression(
170170
template <typename T>
171171
void fill_in_vector(
172172
std::vector<T> &concrete_array,
173-
std::set<std::size_t> &initialized)
173+
const std::set<std::size_t> &initialized)
174174
{
175-
// Pad the concretized values to the left to assign the uninitialized
176-
// values of result.
177-
178-
int last_initialized=-1;
179-
for(const auto &j : initialized)
180-
{
181-
// Start concretizing from the left of `j` and pad from right to left until
182-
// an initialized index (or 0) is reached
183-
std::size_t i=j;
184-
INVARIANT(
185-
concrete_array.size()>j,
186-
"set of initialized indices should not contain out of bound values");
187-
while(i!=0 && i!=last_initialized)
188-
concrete_array[--i]=concrete_array[j];
189-
last_initialized=j;
190-
}
175+
PRECONDITION(!initialized.empty());
176+
auto it=initialized.begin();
177+
PRECONDITION(*initialized.rbegin()==concrete_array.size()-1);
178+
179+
for(std::size_t j=0; j<concrete_array.size(); j++)
180+
if(*it==j)
181+
++it;
182+
else
183+
concrete_array[j]=concrete_array[*it];
191184
}
192185

193186
/// Utility function for concretization of strings. Copies concretized values to

0 commit comments

Comments
 (0)