From 36c9d1f76e69a018f72a8aa85d70c58dd8f0d5cc Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 6 Mar 2013 19:44:09 -0800 Subject: [PATCH] deque: re-insert deleted MODEL_ASSERT() --- chase-lev-deque/main.c | 1 + 1 file changed, 1 insertion(+) diff --git a/chase-lev-deque/main.c b/chase-lev-deque/main.c index 382c62a..f2e8dca 100644 --- a/chase-lev-deque/main.c +++ b/chase-lev-deque/main.c @@ -40,6 +40,7 @@ int user_main(int argc, char **argv) correct=false; if (!correct) printf("a=%d b=%d c=%d\n",a,b,c); + MODEL_ASSERT(correct); return 0; } -- 2.34.1