cpp11.cat read-modify-writes cannot head release sequences

[gonzalobg]

Is the behavior of the following C++11 program well-defined or undefined?

C lb-lna-faddrel-srlx-lacq-sna-cpp11
{ [x] = 0; [y] = 0;  }

P0 (int* x, int* y) {
  int b = *y;
  atomic_fetch_add_explicit(x, 1, memory_order_release);
  atomic_store_explicit(x, 2, memory_order_relaxed);
}

P1 (int* x, int* y) {
  int a = atomic_load_explicit(x, memory_order_acquire);
  if (a != 0) {
    *y = 1;
  }
}

~exists(0:b=1)

The current cpp11.cat model produces Undef.
C++11 6.8.2.1p5 [intro.races] reads:

A release sequence headed by a release operation A on an atomic object M is a maximal contiguous sub-sequence of side effects in the modification order of M, where the first operation is A, and every subsequent operation is performed by the same thread that performed A, or is an atomic read-modify-write operation.

In the example atomic_store_explicit(x, 2, memory_order_relaxed) is performed by the same thread that performed the release operation A (atomic_fetch_add_explicit(x, 1, memory_order_release).

This is therefore a bug in cpp11.cat.