termination.bpl(9,31): Error: Implementation main fails simulation check C at phase 1. Transactions must be separated by a yield.

1 type checking errors detected in termination.bpl