int x1 = 1;
int x2 = 2;
int x3 = 1;

bool flag1 = false;
bool flag2 = false;
bool flag3 = false;

program t1:

void main()
{
	atomic
	{
		x1 = x3+1;
		flag1=true;	
	}
}

program t2:

void main()
{
	atomic
	{
		assume(flag1 == true);
		x2 = x1;
		flag2 = true;
	}
}

program t3:

void main()
{
	atomic
	{
		assume(flag2 == true);
		x3 = x2;
		flag3 = true;	
	}
}

program t4:

void main()
{
	if(flag1 && flag2 && flag3)
	{
		assert(x1 == x2 && x2 == x3); /* OK */
	}
}