From 9b2bb08cb56cc5f41f05ef5be144c89fe9b52c9b Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Thu, 1 Dec 2022 14:57:13 -0500
Subject: [PATCH] Extended precondition of `vListInsertEnd` to prove absence of
 overflows.

---
 list.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/list.c b/list.c
index 5e6dc86f2..5532d8e59 100644
--- a/list.c
+++ b/list.c
@@ -95,7 +95,8 @@ void vListInsertEnd( List_t * const pxList,
     // TODO: Adapt contract and proof to new version of predicates.
 
     /*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals, ?owners) &*&
-        xLIST_ITEM(pxNewListItem, ?val, _, _, ?ow, _);@*/
+        xLIST_ITEM(pxNewListItem, ?val, _, _, ?ow, _) &*&
+        len < INT_MAX;@*/
     /*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals, ?new_owners) &*&
         idx == end
             ? (new_cells == append(cells, singleton(pxNewListItem)) &*&