Calling violate_precondition
Precondition violation not detected
Calling violate_postcondition
Postcondition violation not 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