Invariant of TEST1
Invariant of TEST
Postcondition of weasel
Invariant of TEST1
Invariant of TEST
Execution completed