diff --git a/tasks.c b/tasks.c
index 8ee8ae71a..4f0f498c2 100644
--- a/tasks.c
+++ b/tasks.c
@@ -4136,7 +4136,8 @@ void vTaskSwitchContext( BaseType_t xCoreID )
              interruptsDisabled_f(state) == true &*&
              // opened predicate `coreLocalInterruptInv_p()`
                 pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& 
-                pubTCB_p(gCurrentTCB, 0);
+                pubTCB_p(gCurrentTCB, 0) &*&
+                integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
 
 @*/
 //@ ensures true;
@@ -4176,6 +4177,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
             configASSERT( pxCurrentTCB->uxCriticalNesting == 0 );
         #endif /* VERIFAST */
 
+        //@ open taskISRLockInv();
         if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE )
         {
             /* The scheduler is currently suspended - do not allow a context
diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index f3b3fcbfb..4a0324bec 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -28,7 +28,10 @@ predicate interruptState_p(uint32_t coreID, uint32_t state);
 fixpoint bool interruptsDisabled_f(uint32_t);
 
 predicate coreLocalInterruptInv_p() =
-    pointer(&pxCurrentTCBs[coreID_f], _);
+    pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*&
+    pubTCB_p(currentTCB, 0) &*&
+    integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
+
 
 predicate coreLocalLocked(uint32_t coreID);
 @*/