C test_8

{ y = 0; x = 0; }

void
P0(atomic_int *y, atomic_int *x)
{
    int r0 = 0;
    r0 = atomic_load_explicit(x, memory_order_acquire);
    if (r0 == 1) { *y = 1; }
}

void
P1(atomic_int *y, atomic_int *x)
{ *y = 2; atomic_store_explicit(x, 1, memory_order_release); }

forall ((0:r0 == 0 /\ x == 1 /\ y == 2) \/ (0:r0 == 1 /\ x == 1 /\ y == 1))