deque results
[model-checker-benchmarks.git] / chase-lev-deque-bugfix / testcase4.c
index 93eaa526dc72e34902994ccd9240a8d37ea02f5a..5b0dfb4884e3fd65fed3a83c3ffb14d9d42b2dcf 100644 (file)
@@ -30,8 +30,8 @@ int user_main(int argc, char **argv)
        push(q, 2);
        push(q, 3);
        //thrd_create(&t2, task, 0);
-       //a=take(q);
-       //c=take(q);
+       a=take(q);
+       c=take(q);
        thrd_join(t1);
        //thrd_join(t2);