SmallTests.dfy(34,11): Error: index out of range
Execution trace:
    (0,0): anon0
SmallTests.dfy(65,36): Error: possible division by zero
Execution trace:
    (0,0): anon0
    (0,0): anon13_Then
SmallTests.dfy(66,51): Error: possible division by zero
Execution trace:
    (0,0): anon0
    (0,0): anon13_Else
    (0,0): anon14_Else
SmallTests.dfy(67,22): Error: target object may be null
Execution trace:
    (0,0): anon0
    (0,0): anon13_Then
    (0,0): anon14_Then
    (0,0): anon15_Then
SmallTests.dfy(86,24): Error: target object may be null
Execution trace:
    (0,0): anon0
    SmallTests.dfy(85,5): anon8_LoopHead
    (0,0): anon8_LoopBody
    (0,0): anon9_Then
SmallTests.dfy(120,6): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
    (0,0): anon3
SmallTests.dfy(133,10): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
SmallTests.dfy(135,10): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else
SmallTests.dfy(175,9): Error: assignment may update an object field not in the enclosing context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon22_Else
    (0,0): anon24_Else
    (0,0): anon26_Else
    (0,0): anon28_Then
    (0,0): anon29_Then
    (0,0): anon19
SmallTests.dfy(199,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Then
SmallTests.dfy(206,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon3
    (0,0): anon10_Then
SmallTests.dfy(208,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon3
    (0,0): anon10_Else
SmallTests.dfy(213,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon3
    (0,0): anon10_Then
    (0,0): anon6
    (0,0): anon11_Then
SmallTests.dfy(215,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon3
    (0,0): anon10_Then
    (0,0): anon6
    (0,0): anon11_Else
SmallTests.dfy(261,24): Error BP5002: A precondition for this call might not hold.
SmallTests.dfy(239,30): Related location: This is the precondition that might not hold.
Execution trace:
    (0,0): anon0
    SmallTests.dfy(256,19): anon3_Else
    (0,0): anon2
SmallTests.dfy(366,12): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(376,12): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(386,6): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
SmallTests.dfy(691,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    SmallTests.dfy(688,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    SmallTests.dfy(688,5): anon8_Else
    (0,0): anon9_Then
SmallTests.dfy(712,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon7_Then
    (0,0): anon8_Then
    (0,0): anon3
SmallTests.dfy(296,3): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(290,11): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon18_Else
    (0,0): anon23_Then
    (0,0): anon24_Then
    (0,0): anon15
    (0,0): anon25_Else
SmallTests.dfy(337,12): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon8_Then
    (0,0): anon7
SmallTests.dfy(344,10): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(354,4): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
SmallTests.dfy(398,10): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(401,41): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon7_Else
SmallTests.dfy(562,12): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
    (0,0): anon2
SmallTests.dfy(576,20): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
    (0,0): anon0
    (0,0): anon27_Then
    (0,0): anon28_Then
    (0,0): anon4
    (0,0): anon29_Then
    (0,0): anon30_Then
    (0,0): anon9
    (0,0): anon31_Then
    (0,0): anon32_Then
    (0,0): anon12
SmallTests.dfy(578,15): Error: left-hand sides 1 and 2 may refer to the same location
Execution trace:
    (0,0): anon0
    (0,0): anon27_Then
    SmallTests.dfy(571,18): anon28_Else
    (0,0): anon4
    (0,0): anon29_Else
    (0,0): anon30_Then
    (0,0): anon9
    (0,0): anon31_Else
    (0,0): anon35_Then
    (0,0): anon36_Then
    (0,0): anon37_Then
    (0,0): anon22
    (0,0): anon38_Then
SmallTests.dfy(585,25): Error: target object may be null
Execution trace:
    (0,0): anon0
SmallTests.dfy(598,10): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(622,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
    (0,0): anon0
SmallTests.dfy(645,23): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon8_Then
    (0,0): anon9_Then
    (0,0): anon4
    (0,0): anon10_Then
    (0,0): anon7
SmallTests.dfy(659,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    (0,0): anon6_Then
    (0,0): anon3
SmallTests.dfy(661,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
SmallTests.dfy(674,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 104 verified, 35 errors

Dafny program verifier finished with 0 verified, 0 errors