changes
[model-checker-benchmarks.git] / chase-lev-deque-bugfix / testcase8.c
index d954138db7fb3d70755ebcfe4b81b535a11da7fe..a2387d47496579c08ac4f0a04a61978c68db7641 100644 (file)
@@ -15,23 +15,24 @@ int c;
 
 static void task(void * param) {
        b=steal(q);
-       //c=steal(q);
 }
 
 int user_main(int argc, char **argv)
 {
-       thrd_t t1, t2;
+       thrd_t t1, t2, t3;
        q=create();
 
        push(q, 1);
+       push(q, 2);
+       //push(q, 3);
        thrd_create(&t1, task, 0);
        thrd_create(&t2, task, 0);
+       thrd_create(&t3, task, 0);
        a=take(q);
-       push(q, 2);
-       c=take(q);
-       push(q, 3);
+       //c=take(q);
        thrd_join(t1);
        thrd_join(t2);
+       thrd_join(t3);
 
 /*
        bool correct=true;