======================================
ACCOUNT (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by ACCOUNT)
Successfully verified.
======================================
ACCOUNT.deposit
Successfully verified.
======================================
ACCOUNT.withdraw
Verification failed.

Line: 31. Postcondition balance_decreased may be violated.
======================================
ACCOUNT.transfer
Verification failed.

Line: 49. Postcondition balance_decreased may be violated.