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

bool init=false;
bool deposit_done=false;
bool withdraw_done=false;

program start:

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


program deposit:

void main()
{
	assume(init);
	
	atomic
	{
		balance = balance + y;
		deposit_done = true;
	}
}


program withdraw:

void main()
{
	assume(init);
	
	atomic
	{
		balance = balance - z;
		withdraw_done = true;
	}
}


program check_result:

void main()
{
	assume(init);
	
	atomic
	{		  
		if (deposit_done && withdraw_done)
		{
			assert(balance == (x + y) - z); /* GOOD */
		}
		else
		{
			nop;
		}
	}		
}