From 6a7d36ca9d69293d1d1120663c76fa25b64c02bf Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Sun, 9 Jun 2024 12:28:48 -0400 Subject: [PATCH] queue example working! --- src/examples/queue.broken.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/examples/queue.broken.c b/src/examples/queue.broken.c index b09c8b8a..0799727e 100644 --- a/src/examples/queue.broken.c +++ b/src/examples/queue.broken.c @@ -44,6 +44,7 @@ predicate (datatype seq) IntQueueAux (pointer h, pointer t, i32 lastVal) { return (Seq_Cons{head: lastVal, tail: Seq_Nil{}}); } else { take C = Owned(h); + assert (!is_null(C.next)); // HERE IS THE KEY! take TL = IntQueueAux(C.next, t, lastVal); return (Seq_Cons { head: C.first, tail: TL }); }