Thread-local threads mentioned in postcondition are erroneously deleted

[MattWindsor91]

Example:

C sbsc

{ x = 0; y = 0; }

void P0(atomic_int *x, atomic_int *y) {
  int a;
  atomic_store_explicit(x, 1, memory_order_relaxed);
  a = atomic_load_explicit(y, memory_order_relaxed);
}

void P1(atomic_int *x, atomic_int *y) {
  int b;
  atomic_store_explicit(y, 1, memory_order_relaxed);
  b = atomic_load_explicit(x, memory_order_relaxed);
}

exists (0:a == 0 /\ 1:b == 0)

The generated locations stanza for the litmus test should be x; y; t0a; t1b. Instead, it is x; y, because t0a and t1b are (rightly) treated as local variables, but (wrongly) considered not to be publicly visible.

[MattWindsor91]

I believe I've fixed this, but found a related (XY!) problem: the postcondition itself isn't being propagated properly (see #61).