Checking invariant
Checking invariant
Calling wimp
In wimp
Back from wimp
Checking invariant
Execution completed