WYIL: various bug fixes for translating for loops into the unbounded quantifiers we now have.