Calling violate_precondition
Assertion violation detected
Calling violate_postcondition
Assertion violation detected
Calling violate_invariant
Invariant violation not detected
Calling violate_loop
Loop variant violation not detected
Calling violate_check
Check assertion violation not detected
Execution completed