WYC: bug fix for the way loop invariants are assumed.