Apply.dfy(27,15): Error: assertion violation
Execution trace:
    (0,0): anon0
    Apply.dfy(26,27): anon15_Else
    Apply.dfy(27,19): anon17_Else

Dafny program verifier finished with 6 verified, 1 error