SmallTests.dfy(33,11): Error: index out of range
Execution trace:
    (0,0): anon0
SmallTests.dfy(64,36): Error: possible division by zero
Execution trace:
    (0,0): anon0
    (0,0): anon12_Then
SmallTests.dfy(65,51): Error: possible division by zero
Execution trace:
    (0,0): anon0
    (0,0): anon12_Else
    (0,0): anon3
    (0,0): anon13_Else
SmallTests.dfy(66,22): Error: target object may be null
Execution trace:
    (0,0): anon0
    (0,0): anon12_Then
    (0,0): anon3
    (0,0): anon13_Then
    (0,0): anon6
SmallTests.dfy(85,24): Error: target object may be null
Execution trace:
    (0,0): anon0
    SmallTests.dfy(84,5): anon8_LoopHead
    (0,0): anon8_LoopBody
    (0,0): anon9_Then
SmallTests.dfy(119,6): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
    (0,0): anon3
SmallTests.dfy(132,10): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
SmallTests.dfy(134,10): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else
SmallTests.dfy(174,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(198,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Then
SmallTests.dfy(205,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon3
    (0,0): anon10_Then
SmallTests.dfy(207,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon3
    (0,0): anon10_Else
SmallTests.dfy(212,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(214,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(260,24): Error BP5002: A precondition for this call might not hold.
SmallTests.dfy(238,30): Related location: This is the precondition that might not hold.
Execution trace:
    (0,0): anon0
    SmallTests.dfy(255,19): anon3_Else
    (0,0): anon2
SmallTests.dfy(365,12): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(375,12): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(385,6): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else
SmallTests.dfy(690,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    SmallTests.dfy(687,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    SmallTests.dfy(687,5): anon8_Else
    (0,0): anon9_Then
SmallTests.dfy(711,14): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon7_Then
    (0,0): anon8_Then
    (0,0): anon3
SmallTests.dfy(295,3): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(289,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(336,12): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon8_Then
    (0,0): anon7
SmallTests.dfy(343,10): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(353,4): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else
SmallTests.dfy(397,10): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(400,41): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon6_Else
SmallTests.dfy(561,12): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
    (0,0): anon2
SmallTests.dfy(575,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(577,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(570,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(584,25): Error: target object may be null
Execution trace:
    (0,0): anon0
SmallTests.dfy(597,10): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(621,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
    (0,0): anon0
SmallTests.dfy(644,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(658,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(660,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(673,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