Entering invariant_value
Leaving invariant_value
Execution completed