RankNeg.dfy(10,26): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
    (0,0): anon6_Then
RankNeg.dfy(15,28): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
    (0,0): anon6_Then
RankNeg.dfy(22,31): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
    (0,0): anon6_Then
RankNeg.dfy(32,25): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
    (0,0): anon0
    (0,0): anon5_Else
    (0,0): anon6_Then

Dafny program verifier finished with 1 verified, 4 errors