Bug132.dfy(33,29): Error: receiver argument must be allocated in the state in which the function is invoked
Execution trace:
    (0,0): anon0
    (0,0): anon24_Then
Bug132.dfy(34,29): Error: receiver argument must be allocated in the state in which the function is invoked
Execution trace:
    (0,0): anon0
    (0,0): anon25_Then
Bug132.dfy(37,36): Error: argument must be allocated in the state in which the function is invoked
Execution trace:
    (0,0): anon0
    (0,0): anon26_Then
Bug132.dfy(41,29): Error: receiver argument must be allocated in the state in which the function is invoked
Execution trace:
    (0,0): anon0
    (0,0): anon27_Then

Dafny program verifier finished with 3 verified, 4 errors