diff --git a/tasks.c b/tasks.c
index f32e5df24..8a1994eb2 100644
--- a/tasks.c
+++ b/tasks.c
@@ -5404,11 +5404,9 @@ static void prvResetNextTaskUnblockTime( void )
 
     TaskHandle_t xTaskGetCurrentTaskHandle( void )
     /*@ requires interruptState_p(coreID_f(), ?state) &*&
-             interruptsDisabled_f(state) == true &*&
              pointer(&pxCurrentTCBs[coreID_f], ?taskHandle);
      @*/
     /*@ ensures interruptState_p(coreID_f(), state) &*&
-             interruptsDisabled_f(state) == true &*&
              pointer(&pxCurrentTCBs[coreID_f], taskHandle) &*&
              result == taskHandle;
      @*/