[Civl] Fixed bug in typechecking of yielding loops

[shazqadeer]

Each loop in a yield procedure is allowed to yield up to a yielding layer that is bounded by the disappearance layer of the enclosing yield procedure. This yielding layer N is either specified directly in an annotation on the loop header that looks like

invariant {:yields} {:layer N} true;

or it is inferred.

The inference is done separately for each loop.

The bug was that the result of the inference for one loop was polluting the result for another. The problem is fixed by moving the yieldingLayer variable inside the iteration.