MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int
MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
    MapOutputTypeParams.bpl(13,9): anon0
MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
    MapOutputTypeParams.bpl(25,9): anon0
MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
    MapOutputTypeParams.bpl(34,8): anon0

Boogie program verifier finished with 0 verified, 3 errors