diff --git a/tasks.c b/tasks.c
index ed3664d57..ba0c7b3bd 100644
--- a/tasks.c
+++ b/tasks.c
@@ -1431,6 +1431,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
                 }
             #endif
 
+            /* TODO: Continue proof
+             * For now we stop verification here and concentrate on new
+             * verification target. 
+             */
+            //@ assume(false);
+
             prvAddNewTaskToReadyList( pxNewTCB );
             xReturn = pdPASS;
         }
@@ -1876,10 +1882,10 @@ static void prvInitialiseNewTask( TaskFunction_t pxTaskCode,
 /*-----------------------------------------------------------*/
 
 static void prvAddNewTaskToReadyList( TCB_t * pxNewTCB )
-/*@ requires interruptState_p(?coreID, _) &*&
+/*//@ requires interruptState_p(?coreID, _) &*&
              unprotectedGlobalVars(); 
   @*/
-/*@ ensures true; 
+/*//@ ensures true; 
   @*/
 {
     /* Ensure interrupts don't access the task lists while the lists are being
@@ -5284,8 +5290,8 @@ static void prvResetNextTaskUnblockTime( void )
 #if ( ( INCLUDE_xTaskGetCurrentTaskHandle == 1 ) || ( configUSE_MUTEXES == 1 ) )
 
     TaskHandle_t xTaskGetCurrentTaskHandle( void )
-    //@ requires interruptState_p(?coreID, ?irpState);
-    //@ ensures interruptState_p(coreID, irpState) &*& false;
+    ///@ requires interruptState_p(?coreID, ?irpState);
+    ///@ ensures interruptState_p(coreID, irpState) &*& false;
     {
         TaskHandle_t xReturn;
         uint32_t ulState;
@@ -5662,8 +5668,8 @@ void vTaskYieldWithinAPI( void )
 #if ( portCRITICAL_NESTING_IN_TCB == 1 )
 
     void vTaskEnterCritical( void )
-    //@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars();
-    //@ ensures false;
+    ///@ requires interruptState_p(?coreID, _) &*& unprotectedGlobalVars();
+    ///@ ensures false;
     {
         portDISABLE_INTERRUPTS();
         //@ open unprotectedGlobalVars();