> > $ cat T.litmus
> > C T
> >
> > {}
> >
> > P0(spinlock_t *x)
> > {
> > int r0;
> >
> > spin_lock(x);
> > spin_unlock(x);
> > r0 = spin_is_locked(x);
> > }
>
> No "exists" clause? Maybe that's your problem.
Nope, that doesn't seem to be it. (Same result after adding one.)
Andrea
