git-issue-1163.dfy.expect

git-issue-1163.dfy(7,17): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
git-issue-1163.dfy(21,42): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked
git-issue-1163.dfy(23,44): Error: argument could not be proved to be allocated in the state in which the function is invoked
git-issue-1163.dfy(27,40): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked

Dafny program verifier finished with 2 verified, 3 errors