Skip to content

Commit

Permalink
fix iterator in freeze_lazy_contraints
Browse files Browse the repository at this point in the history
Also change for loops

Fixes:diffblue#1581
  • Loading branch information
polgreen committed Dec 3, 2017
1 parent ab9e585 commit aa0e2e3
Showing 1 changed file with 4 additions and 7 deletions.
11 changes: 4 additions & 7 deletions src/solvers/refinement/refine_arrays.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -121,16 +121,13 @@ void bv_refinementt::freeze_lazy_constraints()
if(!lazy_arrays)
return;

for(std::list<lazy_constraintt>::iterator
l_it=lazy_array_constraints.begin();
l_it!=lazy_array_constraints.end(); ++l_it)
for(const auto &constraint : lazy_array_constraints)
{
std::set<symbol_exprt> symbols;
find_symbols(l_it->lazy, symbols);
for(std::set<symbol_exprt>::const_iterator it=symbols.begin();
it!=symbols.end(); ++it)
find_symbols(constraint.lazy, symbols);
for(const auto &symbol : symbols)
{
bvt bv=convert_bv(l_it->lazy);
const bvt bv=convert_bv(symbol);
forall_literals(b_it, bv)
if(!b_it->is_constant())
prop.set_frozen(*b_it);
Expand Down

0 comments on commit aa0e2e3

Please sign in to comment.