deque: re-insert deleted MODEL_ASSERT()
authorBrian Norris <banorris@uci.edu>
Thu, 7 Mar 2013 03:44:09 +0000 (19:44 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 7 Mar 2013 03:44:09 +0000 (19:44 -0800)
chase-lev-deque/main.c

index 382c62a..f2e8dca 100644 (file)
@@ -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;
 }