Classes.dfy(41,6): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    (0,0): anon11_Then
    (0,0): anon3
    (0,0): anon12_Then
    (0,0): anon13_Else
    (0,0): anon14_Else

Dafny program verifier finished with 6 verified, 1 error