From: Brian Norris <banorris@uci.edu>
Date: Thu, 7 Mar 2013 03:10:36 +0000 (-0800)
Subject: deque: add MODEL_ASSERT(), fixup #include's
X-Git-Tag: oopsla2013-final~27^2^2
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=commitdiff_plain;h=ad2809cd62aeacf73e1bd4e5f57ef02b913190a5

deque: add MODEL_ASSERT(), fixup #include's
---

diff --git a/chase-lev-deque/main.c b/chase-lev-deque/main.c
index ee69867..c744b47 100644
--- a/chase-lev-deque/main.c
+++ b/chase-lev-deque/main.c
@@ -3,6 +3,9 @@
 #include <stdio.h>
 #include <threads.h>
 #include <stdatomic.h>
+#include <stdio.h>
+
+#include "model-assert.h"
 
 #include "deque.h"
 
@@ -25,7 +28,9 @@ int user_main(int argc, char **argv)
 	push(q, 2);
 	b=take(q);
 	thrd_join(t);
-	if (a+b!=3)
-		printf("a=%d b=%d\n",a,b);
+
+	printf("a=%d b=%d\n",a,b);
+	MODEL_ASSERT(a + b == 3);
+
 	return 0;
 }