diff --git a/tasks.c b/tasks.c
index 9c048fcc4..8f14ca882 100644
--- a/tasks.c
+++ b/tasks.c
@@ -965,16 +965,11 @@ static void prvYieldForTask( TCB_t * pxTCB,
                     // opened predicate `coreLocalInterruptInv_p()`
                         [0.5]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& 
                         integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) 
-//                        coreLocalSeg_TCB_p(gCurrentTCB, 0)
-//                    &*&
-                    // read access to current task's stack pointer, etc
-//                        prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack)
                 &*&
                 // additional knowledge
                     (xTaskScheduled == 0
                         ? (0 <= uxCurrentPriority &*& uxCurrentPriority <= gTopReadyPriority &*&
                            gTopReadyPriority < configMAX_PRIORITIES
-        //                 0 <= uxCurrentPriority &*& uxCurrentPriority < configMAX_PRIORITIES
                         ) : true
                     );
         @*/
@@ -1078,10 +1073,6 @@ static void prvYieldForTask( TCB_t * pxTCB,
                             foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates))
                         &*&
                         subset(gOwners, gTasks) == true &*&
-                        (uxCurrentPriority == 0
-                            ? length(gCells) == configNUM_CORES
-                            : true
-                        ) &*&
                         List_array_p(&pxReadyTasksLists, uxCurrentPriority, gPrefCellLists,
                                      gPrefOwnerLists) &*&
                         List_array_p(&pxReadyTasksLists + uxCurrentPriority + 1, 
diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h
index 6893ebb20..ac971fe62 100644
--- a/verification/verifast/proof/ready_list_predicates.h
+++ b/verification/verifast/proof/ready_list_predicates.h
@@ -15,10 +15,7 @@ predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists,
     configMAX_PRIORITIES == length(gCellLists) &*&
     List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, 
                  gCellLists, gOwnerLists) &*&
-    length(gCellLists) == length(gOwnerLists) &*&
-    // List of priority 0 always contains the idle task and the end marker
-    // nothing else
-    length( nth(0, gCellLists) ) == configNUM_CORES;
+    length(gCellLists) == length(gOwnerLists);
 
 
 predicate List_array_p(List_t* array, int size, 
@@ -139,7 +136,6 @@ lemma void closeUnchanged_readyLists(list<list<struct xLIST_ITEM*> > cellLists,
 requires 
     configMAX_PRIORITIES == length(cellLists) &*&
     configMAX_PRIORITIES == length(ownerLists) &*&
-    length( nth(0, cellLists) ) == configNUM_CORES &*&
     List_array_p(&pxReadyTasksLists, ?gIndex, ?gPrefCellLists, ?gPrefOwnerLists) &*&
     gIndex < length(cellLists) &*&
     xLIST(&pxReadyTasksLists + gIndex, ?gLen, _, _, ?gCells, ?gVals, ?gOwners) &*&
@@ -181,7 +177,6 @@ lemma void closeReordered_readyLists(list<list<struct xLIST_ITEM*> > cellLists,
 requires
     configMAX_PRIORITIES == length(cellLists) &*&
     configMAX_PRIORITIES == length(ownerLists) &*&
-    length( nth(0, cellLists) ) == configNUM_CORES &*&
     List_array_p(&pxReadyTasksLists, ?gIndex, ?gPrefCellLists, ?gPrefOwnerLists) &*&
     gIndex < length(cellLists) &*&
     xLIST(&pxReadyTasksLists + gIndex, ?gLen, _, _, reorderedCells, _, reorderedOwners) &*&
@@ -220,7 +215,6 @@ ensures
         assert( nth(0, gPrefCellLists) == nth(0, cellLists) );
     }
     assert( length(nth(0, gReorderedCellLists)) == length(nth(0, cellLists)) );
-    assert( length(nth(0, gReorderedCellLists)) == configNUM_CORES );
 
     close readyLists_p(gReorderedCellLists, gReorderedOwnerLists);
 
@@ -256,7 +250,6 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
             &*&
             length(gCellLists) == configMAX_PRIORITIES &*&
             length(gOwnerLists) == configMAX_PRIORITIES &*&
-            length(nth(0, gCellLists)) == configNUM_CORES &*&
             0 <= gOffset &*& gOffset < length(gCellLists) 
         &*&
         // current ready list