ModifyStmt.dfy(27,13): Error: assertion violation
Execution trace:
    (0,0): anon0
ModifyStmt.dfy(42,4): Error: modify statement may violate context's modifies clause
Execution trace:
    (0,0): anon0
ModifyStmt.dfy(48,4): Error: modify statement may violate context's modifies clause
Execution trace:
    (0,0): anon0
ModifyStmt.dfy(61,4): Error: modify statement may violate context's modifies clause
Execution trace:
    (0,0): anon0
ModifyStmt.dfy(70,13): Error: assertion violation
Execution trace:
    (0,0): anon0
ModifyStmt.dfy(89,13): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Then
    ModifyStmt.dfy(81,7): anon10_LoopHead
    (0,0): anon10_LoopBody
    ModifyStmt.dfy(81,7): anon11_Else
    (0,0): anon12_Then
    (0,0): anon8
ModifyStmt.dfy(99,13): Error: assertion violation
Execution trace:
    (0,0): anon0
ModifyStmt.dfy(110,13): Error: assertion violation
Execution trace:
    (0,0): anon0
ModifyStmt.dfy(122,15): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
ModifyStmt.dfy(134,6): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
ModifyStmt.dfy(172,14): Error: assertion violation
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 25 verified, 11 errors