diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
index ef12b6819..e5ff0b1b0 100644
--- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
+++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
@@ -2139,11 +2139,6 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
 /*-----------------------------------------------------------*/
 
 static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
-/*//@ requires interruptState_p(?coreID, _) &*&
-             unprotectedGlobalVars(); 
-  @*/
-/*//@ ensures true; 
-  @*/
 {
     /* Ensure interrupts don't access the task lists while the lists are being
      * updated. */