deque: bug fix...method could return empty
[model-checker-benchmarks.git] / chase-lev-deque / main.c
index 64d0444..77ea5a8 100644 (file)
@@ -21,7 +21,9 @@ int user_main(int argc, char **argv)
        thrd_create(&t, task, 0);
        push(q, 1);
        push(q, 2);
-       b=take(q);
+       do {
+               b=take(q);
+       }       while(b==EMPTY);
        thrd_join(t);
        if (a+b!=3)
                printf("a=%d b=%d\n",a,b);