From 61bffc4617152d723eafc1fcd1bb99c6e500b30a Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Sun, 4 Dec 2022 10:46:05 -0500
Subject: [PATCH] Adapted loop invariant to reflect potential change of state
 lists.

---
 tasks.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tasks.c b/tasks.c
index 342a42ffb..01ae07e4f 100644
--- a/tasks.c
+++ b/tasks.c
@@ -988,7 +988,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
             #endif
 
             //@ open taskISRLockInv_p();
-            //@ assert( exists_in_taskISRLockInv_p(?gTasks, ?gStates) );
+            //@ assert( exists_in_taskISRLockInv_p(?gTasks, ?gStates0) );
 
             //@ open readyLists_p(?gCellLists, ?gOwnerLists);
             //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
@@ -1051,7 +1051,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                         mem(pxTaskItem, gCells) == true &*&
                         xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*&
                         gSize > 0 &*&
-                        exists_in_taskISRLockInv_p(gTasks, gStates)
+                        exists_in_taskISRLockInv_p(gTasks, ?gStates)
                         &*&
                         // Read permissions for every task
                             foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates))