From ad2809cd62aeacf73e1bd4e5f57ef02b913190a5 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Wed, 6 Mar 2013 19:10:36 -0800
Subject: [PATCH 1/1] deque: add MODEL_ASSERT(), fixup #include's

---
 chase-lev-deque/main.c | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

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;
 }
-- 
2.34.1