SmallTests.dfy(507,4): Warning: /!\ No trigger covering all quantified variables found.
SmallTests.dfy(34,10): Error: index out of range
Execution trace:
    (0,0): anon0
SmallTests.dfy(65,35): Error: possible division by zero
Execution trace:
    (0,0): anon0
    (0,0): anon13_Then
SmallTests.dfy(66,50): Error: possible division by zero
Execution trace:
    (0,0): anon0
    (0,0): anon13_Else
    (0,0): anon14_Else
SmallTests.dfy(67,21): 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,23): 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,5): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
    (0,0): anon3
SmallTests.dfy(133,9): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
SmallTests.dfy(135,9): Error: call may violate context's modifies clause
Execution trace:
    (0,0): anon0
    (0,0): anon3_Else
SmallTests.dfy(175,8): 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,13): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Then
SmallTests.dfy(206,13): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon3
    (0,0): anon10_Then
SmallTests.dfy(208,13): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon9_Else
    (0,0): anon3
    (0,0): anon10_Else
SmallTests.dfy(213,13): 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,13): 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,23): Error BP5002: A precondition for this call might not hold.
SmallTests.dfy(239,29): 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(367,11): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(377,11): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(387,5): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
SmallTests.dfy(692,13): Error: assertion violation
Execution trace:
    (0,0): anon0
    SmallTests.dfy(689,5): anon7_LoopHead
    (0,0): anon7_LoopBody
    SmallTests.dfy(689,5): anon8_Else
    (0,0): anon9_Then
SmallTests.dfy(713,13): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon7_Then
    (0,0): anon8_Then
    (0,0): anon3
SmallTests.dfy(296,2): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(290,10): Related location: This is the postcondition that might not hold.
SmallTests.dfy(290,40): Related location
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(338,11): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon7_Then
    (0,0): anon6
SmallTests.dfy(345,9): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(355,3): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else
SmallTests.dfy(399,9): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(402,40): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon7_Else
SmallTests.dfy(563,11): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon3_Then
    (0,0): anon2
SmallTests.dfy(577,19): 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(579,14): Error: left-hand sides 1 and 2 may refer to the same location
Execution trace:
    (0,0): anon0
    (0,0): anon27_Then
    SmallTests.dfy(572,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(586,24): Error: target object may be null
Execution trace:
    (0,0): anon0
SmallTests.dfy(599,9): Error: assertion violation
Execution trace:
    (0,0): anon0
SmallTests.dfy(623,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
    (0,0): anon0
SmallTests.dfy(646,22): 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(660,9): 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(662,9): 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(675,8): 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
SmallTests.dfy.tmp.dprint.dfy(369,4): Warning: /!\ No trigger covering all quantified variables found.

Dafny program verifier finished with 0 verified, 0 errors