C C-CO+o-o+o-o.litmus { } P0(int *x) { WRITE_ONCE(*x, 3); WRITE_ONCE(*x, 4); } P1(int *x) { int r1; int r2; r1 = READ_ONCE(*x); r2 = READ_ONCE(*x); } exists (1:r1=4 /\ 1:r2=3)