From 546aac34d0cbc07c053c579fad1db268718ff3b3 Mon Sep 17 00:00:00 2001
From: Anthony Berg <smyalygames@gmail.com>
Date: Thu, 7 Mar 2024 16:35:49 +0000
Subject: [PATCH] fix(formal): stack underflow for index_of_item

---
 formal/checklist.vdmsl | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/formal/checklist.vdmsl b/formal/checklist.vdmsl
index ca0e513..6ebe18b 100644
--- a/formal/checklist.vdmsl
+++ b/formal/checklist.vdmsl
@@ -122,6 +122,8 @@ functions
             index_of_item(i, tl a) + 1
         pre
             len a > 0
+            -- Checks if the last item in the aircraft is the item that is being searched for
+            and (len a = 1 and a(1).name = i)
         post
             -- Checks that the index is correct
             --TODO this does not check if it is the first item in the list