======================================
A_MAPS (invariant admissibility)
Successfully verified.
======================================
ANY.default_create (creator, inherited by A_MAPS)
Successfully verified.
======================================
A_MAPS.good
Successfully verified.
======================================
A_MAPS.good1
Successfully verified.
======================================
A_MAPS.bad
Verification failed.

Line: 94. Precondition may be violated on invocation of {MML_MAP}.item.
--------------------------------------
Line: 97. Precondition may be violated on invocation of {MML_MAP}.image.
--------------------------------------
Line: 101. Precondition may be violated on invocation of {MML_MAP}.sequence_image.