diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md b/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md
index 8d08e1e47..37d503b6d 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md
@@ -1,9 +1,6 @@
 This directory contains the bulk of VeriFast formalizations and proofs.
 
 
-
-
-
 # Directory Structure
 ```
 ├── lock_predicates.h
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h
index 5941621d5..e146e9f83 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h
@@ -150,7 +150,6 @@ predicate _taskISRLockInv_p(UBaseType_t gTopReadyPriority) =
         // (RP-Current) Read permission for task currently scheduled on this core
         // (RP-All) + (RP-Current) => Write permission for scheduled task
             [1/2]TCB_runState_p(gCurrentTCB, ?gCurrentTCB_state) &*&
-//            gCurrentTCB_state != taskTASK_NOT_RUNNING &*&
             (gCurrentTCB_state == coreID_f() || gCurrentTCB_state == taskTASK_YIELDING) &*&
             nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state
         &*&
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h
index bb22ab5d0..3e74d976f 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h
@@ -8,6 +8,10 @@
 
 
 /*@
+// This predicate represents the global ready lists, i.e., the global array
+// `pxReadyTasksLists` in `tasks.c`.
+// Each index `p` stores a cyclic doubly linked list containing all tasks
+// of priority `p` that are ready to run.
 predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists,
                        list<list<void*> > gOwnerLists) =
     configMAX_PRIORITIES == length(gCellLists) &*&
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
index 3f600c320..78901121f 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
@@ -904,12 +904,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                  &*&
                  // opened predicate `coreLocalInterruptInv_p()`
                     [1/2]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB0) &*& 
-                    integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _)
-//                    TCB_criticalNesting_p(gCurrentTCB0, 0)
-                 &*&
-                 // read access to current task's stack pointer, etc
-//                    TCB_stack_p(gCurrentTCB0, ?ulFreeBytesOnStack);
-                true;
+                    integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
     @*/
     /*@ ensures  0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
                  xCoreID == coreID_f() &*&
@@ -922,12 +917,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                  &*&
                  // opened predicate `coreLocalInterruptInv_p()`
                     [1/2]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& 
-                    integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _)
-//                    TCB_criticalNesting_p(gCurrentTCB, 0)
-                 &*&
-                 // read access to current task's stack pointer, etc
-//                    TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack);
-                true;
+                    integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
     @*/
     {
         //@ open taskISRLockInv_p();
@@ -1422,12 +1412,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
             // @ append_take_nth_drop(uxCurrentPriority, gCellLists);
             // @ append_take_nth_drop(uxCurrentPriority, gOwnerLists);
 
-
-//            //@ assert( List_array_p(&pxReadyTasksLists, ?gSize2, ?gCellLists2, ?gOwnerLists2) );
-
-
             //@ assert( exists_in_taskISRLockInv_p(gTasks, ?gStates) );
-  //          //@ close readyLists_p(gCellLists2, gOwnerLists2);
             //@ close _taskISRLockInv_p(uxTopReadyPriority);
         }   // outer loop end
 
@@ -4403,7 +4388,6 @@ void vTaskSwitchContext( BaseType_t xCoreID )
             &*&
             // read access to current task's stack pointer, etc
                 TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack);
-            // Remark: the part of the post condition relating to TCBs will have to change.
 @*/
 {
     /* Acquire both locks: