diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h
index c4592b2d0..615c7451c 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h
@@ -85,46 +85,7 @@ predicate isrLockInv_p();
 fixpoint int taskISRLockID_f();
 
 predicate taskISRLockInv_p() = 
-    // Access to global variables
-        [0.5]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
-        integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*&
-        integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _)
-    &*&
-    // top ready priority must be in range
-        integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&
-        0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES
-    &*&
-    // tasks / TCBs
-        exists_in_taskISRLockInv_p(?gTasks, ?gStates)
-        &*&
-        // (RP-All) Read permissions for every task
-        //          and recording of task states in state list
-        // (∀t ∈ gTasks. 
-        //      [1/2]sharedSeg_TCB_p(t, _))
-        // ∧ 
-        // ∀i. ∀t. gTasks[i] == t -> gStates[i] == t->xTaskRunState    
-            foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates))
-        &*&
-        // (RP-Current) Read permission for task currently scheduled on this core
-        // (RP-All) + (RP-Current) => Write permission for scheduled task
-            [1/2]sharedSeg_TCB_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
-        &*&
-        // (RP-Unsched) Read permissions for unscheduled tasks
-        // (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks
-        // ∀t ∈ tasks. t->xTaskState == taskTASK_NOT_RUNNING
-        //             -> [1/2]shared_TCB_p(t, taskTASK_NOT_RUNNING)
-            foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates))
-        &*&
-        readyLists_p(?gCellLists, ?gOwnerLists) 
-        &*&
-        // gTasks contains all relevant tasks
-            mem(gCurrentTCB, gTasks) == true
-            &*&
-            // ∀l ∈ gOwnerLists. l ⊆ gTasks
-                forall(gOwnerLists, (superset)(gTasks)) == true;
+    _taskISRLockInv_p(_);
 
 
 // Auxiliary predicate. Equal to the lock invariant above but exposes
diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
index 33a0f507c..c68514334 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
@@ -932,7 +932,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
     @*/
     {
         //@ open taskISRLockInv_p();
-        //@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority0) );
+        //@ open _taskISRLockInv_p(?gTopReadyPriority0);
+        //@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, gTopReadyPriority0) );
         //@ assert( gTopReadyPriority0 == uxTopReadyPriority);
         UBaseType_t uxCurrentPriority = uxTopReadyPriority;
         BaseType_t xTaskScheduled = pdFALSE;
@@ -1390,6 +1391,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
                 // @ append_take_nth_drop(uxCurrentPriority, gOwnerLists);
                 
                 // @ close readyLists_p(gCellLists2, gOwnerLists2);
+                //@ close _taskISRLockInv_p(_);
                 //@ close taskISRLockInv_p();
                 return pdFALSE;
             }
@@ -1508,7 +1510,6 @@ static void prvYieldForTask( TCB_t * pxTCB,
             #endif /* if ( configUSE_CORE_AFFINITY == 1 ) */
         #endif /* if ( configNUM_CORES > 1 ) */
 
-        //@ open _taskISRLockInv_p(_);
         //@ close taskISRLockInv_p();
         return pdTRUE;
     }
@@ -4442,11 +4443,13 @@ void vTaskSwitchContext( BaseType_t xCoreID )
         #endif /* VERIFAST */
 
         //@ open taskISRLockInv_p();
+        //@ open _taskISRLockInv_p(_);
         if( uxSchedulerSuspended != ( UBaseType_t ) pdFALSE )
         {
             /* The scheduler is currently suspended - do not allow a context
              * switch. */
             xYieldPendings[ xCoreID ] = pdTRUE;
+            //@ close _taskISRLockInv_p(_);
             //@ close taskISRLockInv_p();
         }
         else
@@ -4494,6 +4497,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
 
             /* Select a new task to run using either the generic C or port
              * optimised asm code. */
+            //@ close _taskISRLockInv_p(_);
             //@ close taskISRLockInv_p();
             ( void ) prvSelectHighestPriorityTask( xCoreID );
             traceTASK_SWITCHED_IN();