TEST2 invariant
TEST3 invariant
TEST1 invariant
Execution completed