Types.12.expect

text.dfy(10,27): Error: argument at index 0 for parameter 'c' could not be proved to be allocated in the two-state function's previous state -- if you add 'new' before the parameter declaration, like 'new c: Cell', arguments can refer to expressions possibly unallocated in the previous state

Dafny program verifier finished with 2 verified, 1 error