C auto/C-RW-G+RW-R+RW-G+RW-R-relacq
{
}

P0(int *x0, int *x1, int *gpstart01, int *csend01, int *csend02)
{
	r1 = READ_ONCE(*x0);
	smp_mb();
	smp_store_release(gpstart01, 1);
	smp_mb();
	r60101 = smp_load_acquire(csend01);
	r60201 = smp_load_acquire(csend02);
	smp_mb();
	WRITE_ONCE(*x1, 1);
}


P1(int *x1, int *x2, int *gpstart01, int *gpstart02, int *csend01)
{
	r50101 = smp_load_acquire(gpstart01);
	r50201 = smp_load_acquire(gpstart02);
	r1 = READ_ONCE(*x1);
	WRITE_ONCE(*x2, 1);
	smp_store_release(csend01, 1);
}


P2(int *x2, int *x3, int *gpstart02, int *csend01, int *csend02)
{
	r1 = READ_ONCE(*x2);
	smp_mb();
	smp_store_release(gpstart02, 1);
	smp_mb();
	r60102 = smp_load_acquire(csend01);
	r60202 = smp_load_acquire(csend02);
	smp_mb();
	WRITE_ONCE(*x3, 1);
}


P3(int *x0, int *x3, int *gpstart01, int *gpstart02, int *csend02)
{
	r50102 = smp_load_acquire(gpstart01);
	r50202 = smp_load_acquire(gpstart02);
	r1 = READ_ONCE(*x3);
	WRITE_ONCE(*x0, 1);
	smp_store_release(csend02, 1);
}

exists ( (0:r1=1 /\ 1:r1=1 /\ 2:r1=1 /\ 3:r1=1)
 /\ (1:r50101=1 \/ 0:r60101=1) /\ (3:r50102=1 \/ 0:r60201=1)
 /\ (1:r50201=1 \/ 2:r60102=1) /\ (3:r50202=1 \/ 2:r60202=1) )