freeze lazy constraints, unused variable?

[polgreen]

This is a question rather than a bug report, but I wasn't sure who to direct the question to.

I'm looking at the function bv_refinementt::freeze_lazy_constraints()
https://github.com/diffblue/cbmc/blob/develop/src/solvers/refinement/refine_arrays.cpp#L118-L139

I don't really understand what this loop is doing:

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)
{
  bvt bv=convert_bv(l_it->lazy);
  forall_literals(b_it, bv)
    if(!b_it->is_constant())
      prop.set_frozen(*b_it);
}

The iterator "it" for the outer loop is never used, and calling set_frozen multiple times is the same as calling it once, so I think the code would do the same thing if the loop was removed?

I tried removing the outer for loop completely and all the regression tests pass.

[romainbrenguier]

Strange, there is something wrong here. I guess it was meant to be bvt bv=convert_bv(*it); on the 5th line, but I think @kroening should confirm that.

[kroening]

Yes, *it seems the thing

[polgreen]

Ok, I've made that change in my version now. Pull request might have been slightly pointless, but it's here: #1588