deque: bug fix...method could return empty

[model-checker-benchmarks.git] / chase-lev-deque / main.c

diff --git a/chase-lev-deque/main.c b/chase-lev-deque/main.c
index 64d044450a93c5bccee63243ef5b279b6f622ea0..77ea5a850451d06c9e66eb627ade7ab4dd0e6946 100644 (file)
--- a/chase-lev-deque/main.c
+++ b/chase-lev-deque/main.c
@@ -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);