CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable
CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable
2 resolution/type errors detected in CallStmtTests.dfy