Basics.dfy(45,14): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon3_Else Basics.dfy(69,42): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon13_Then (0,0): anon14_Then (0,0): anon15_Then Basics.dfy(69,72): anon16_Else Basics.dfy(69,82): anon17_Else Basics.dfy(69,95): anon18_Else (0,0): anon12 Basics.dfy(113,16): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon10_Then Basics.dfy(132,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value Execution trace: (0,0): anon0 (0,0): anon10_Then (0,0): anon3 (0,0): anon11_Then (0,0): anon6 (0,0): anon12_Then (0,0): anon9 Basics.dfy(146,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value Execution trace: (0,0): anon0 Basics.dfy(158,19): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon11_Then Basics.dfy(160,10): Error: assignment may update an object not in the enclosing context's modifies clause Execution trace: (0,0): anon0 (0,0): anon3 Basics.dfy(160,10): Error: target object may be null Execution trace: (0,0): anon0 (0,0): anon3 Basics.dfy(165,12): Error: left-hand sides 0 and 1 may refer to the same location Execution trace: (0,0): anon0 (0,0): anon11_Then (0,0): anon3 (0,0): anon12_Then Basics.dfy(176,15): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon11_Then (0,0): anon3 (0,0): anon12_Else (0,0): anon6 (0,0): anon13_Then (0,0): anon8 (0,0): anon14_Then Basics.dfy(238,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value Execution trace: (0,0): anon0 Basics.dfy(429,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon4_Then (0,0): anon3 Basics.dfy(440,19): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon4_Else Basics.dfy(442,12): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon4_Then (0,0): anon3 Dafny program verifier finished with 61 verified, 14 errors