int x;
int y;
int z;
int balance;

bool i=false;
bool deposit_done=false;
bool withdraw_done=false;

program start:

void main()
{
	  x = ??;
	  y = ??;
	  z = ??;
  	  
	  atomic {balance = x;}
	  i = true;
}

program deposit:

void main()
{
	assume(i);

	atomic
	{
		balance = balance + y;
		deposit_done = true;
	}
}

program withdraw:

void main()
{
	assume(i);

	atomic
	{
		balance = balance - z;
		withdraw_done = true;
	}
}

program check_result:

void main()
{
	assume(i);

	atomic
	{		  
		if (deposit_done && withdraw_done)
		{
			assert(balance == (x - y) - z); /* BAD */
		}
		else
		{
			nop;
		}
	}		
}