diff --git a/src/example-archive/simple-examples/working/list_preds.h b/src/example-archive/simple-examples/working/list_preds.h index 90f67d16..61008b04 100644 --- a/src/example-archive/simple-examples/working/list_preds.h +++ b/src/example-archive/simple-examples/working/list_preds.h @@ -25,11 +25,10 @@ datatype seq { /*@ predicate (datatype seq) IntListSeg(pointer p, pointer tail) { - if (addr_eq(p,tail)) { + if (ptr_eq(p,tail)) { return Seq_Nil{}; } else { take H = Owned(p); - assert (is_null(H.next) || H.next != NULL); take tl = IntListSeg(H.next, tail); return (Seq_Cons { val: H.val, next: tl }); } @@ -62,4 +61,4 @@ function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) { // } // } // } -// @*/ \ No newline at end of file +// @*/