X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=ms-queue%2Fmain.c;h=b541b010c2837d04e798b6db73a2eb4d3dbc4f31;hb=6ad55b673cd0430f7c525f0d19e4fff5b94c971e;hp=c09470de2b22f3760d4b3e2fcb2ee3c3b3e0b195;hpb=688f4bdb69ca33ce415fff112af8000a669466e2;p=model-checker-benchmarks.git

diff --git a/ms-queue/main.c b/ms-queue/main.c
index c09470d..b541b01 100644
--- a/ms-queue/main.c
+++ b/ms-queue/main.c
@@ -44,7 +44,6 @@ int user_main(int argc, char **argv)
 	int i;
 	int *param;
 	unsigned int in_sum = 0, out_sum = 0;
-	int zero = 0;
 
 	queue = calloc(1, sizeof(*queue));
 	MODEL_ASSERT(queue);
@@ -69,12 +68,9 @@ int user_main(int argc, char **argv)
 	}
 	for (i = 0; i < num_threads; i++)
 		printf("input[%d] = %u\n", i, input[i]);
-	for (i = 0; i < num_threads; i++) {
-		if (output[i] == 0)
-			zero = 1; /* A zero result means queue was empty */
+	for (i = 0; i < num_threads; i++)
 		printf("output[%d] = %u\n", i, output[i]);
-	}
-	MODEL_ASSERT(in_sum == out_sum || zero);
+	MODEL_ASSERT(in_sum == out_sum);
 
 	free(param);
 	free(threads);