class TEST feature make do from invariant True until False loop variant 1 end from invariant True variant 2 until False loop end from invariant a :True until False loop variant b :1 end from invariant a :True variant b :2 until False loop end end end