source: CIVL/examples/pthread/cprover/29_conditionals_vs_true.c@ bb03188

#include <pthread.h>

#define assume(e) __VERIFIER_assume(e)
#define assert_nl(e) { if(!(e)) { goto ERROR; } }
#define assert(e) { if(!(e)) { ERROR: goto ERROR; (void)0; } }

int m = 0;

void __VERIFIER_atomic_acquire()
{
        assume(m==0);
        m = 1;
}

void __VERIFIER_atomic_release()
{
        assume(m==1);
        m = 0;
}

void* thr1(void* arg)
{
        int x;
        int y;

        x = __VERIFIER_nondet_int();
        y = __VERIFIER_nondet_int();

        int z;
        __VERIFIER_atomic_acquire();
        if(x == y)
        {
                z = 0;
        } else {
                z = 1;
        }

        if(z == 0)
        {
                assert_nl(x == y);
        } else {
                assert(x != y);
        }
        __VERIFIER_atomic_release();

        return 0;

}

int main()
{
  pthread_t t;

        while(1)
        {
          pthread_create(&t, 0, thr1, 0);
        }
}