Is this a false positive?

genmc-lkmm-race.c

// run: genmc -mo -lkmm genmc-lkmm-race.c
#include <pthread.h>
#include <lkmm.h>

int spin;
int lock;

void* run1(void *arg)
{
	spin = 0;
#if 1 // FAILS, why?
	smp_wmb();
	WRITE_ONCE(lock, 1);
#elif 0 // OK
	smp_mb();
	WRITE_ONCE(lock, 1);
#else // OK
	smp_store_release(&lock, 1);
#endif
	return 0;
}

void *run0(void *arg)
{
#if 1 // both options are the same
	if (READ_ONCE(lock) != 0) {
		smp_mb();
		spin = 1;
	}
#else
	if (smp_load_acquire(&lock) != 0)
		spin = 1;
#endif
	return 0;
}

int main()
{
	pthread_t t;
	pthread_create(&t, 0, run1, 0);
	run0(0);    
	pthread_join(t, 0);
	return 0;
}