OneShot.dfy(20,11): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    OneShot.dfy(13,8): anon5_Else
    (0,0): anon6_Then
OneShot.dfy(22,11): Error: assertion violation
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    OneShot.dfy(13,8): anon5_Else
    (0,0): anon6_Else
OneShot.dfy(22,12): Error: possible violation of function precondition
Execution trace:
    (0,0): anon0
    (0,0): anon5_Then
    OneShot.dfy(13,8): anon5_Else
    (0,0): anon6_Else

Dafny program verifier finished with 1 verified, 3 errors