SeparateVerification0.bpl(19,6): Error: undeclared identifier: y
1 name resolution errors detected in SeparateVerification0.bpl