TypeParameters.dfy(47,21): Error: assertion violation
Execution trace:
    (0,0): anon0
TypeParameters.dfy(69,26): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
    (0,0): anon2
TypeParameters.dfy(156,11): Error: assertion violation
TypeParameters.dfy(156,27): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon20_Then
    TypeParameters.dfy(156,32): anon21_Else
    (0,0): anon5
TypeParameters.dfy(158,11): Error: assertion violation
TypeParameters.dfy(158,32): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon23_Then
    TypeParameters.dfy(158,37): anon24_Else
    (0,0): anon11
TypeParameters.dfy(160,11): Error: assertion violation
TypeParameters.dfy(160,19): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon25_Then
TypeParameters.dfy(162,11): Error: assertion violation
TypeParameters.dfy(147,4): Related location
TypeParameters.dfy(162,20): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon26_Then
TypeParameters.dfy(164,11): Error: assertion violation
TypeParameters.dfy(149,7): Related location
Execution trace:
    (0,0): anon0
    (0,0): anon27_Then
TypeParameters.dfy(178,14): Error BP5005: This loop invariant might not be maintained by the loop.
TypeParameters.dfy(178,37): Related location
Execution trace:
    (0,0): anon0
    TypeParameters.dfy(171,3): anon16_LoopHead
    (0,0): anon16_LoopBody
    TypeParameters.dfy(171,3): anon17_Else
    (0,0): anon19_Then
    TypeParameters.dfy(177,3): anon20_LoopHead
    (0,0): anon20_LoopBody
    TypeParameters.dfy(177,3): anon21_Else
    TypeParameters.dfy(177,3): anon23_Else

Dafny program verifier finished with 63 verified, 8 errors