diff --git a/tasks.c b/tasks.c
index 20418e47a..c847a1457 100644
--- a/tasks.c
+++ b/tasks.c
@@ -895,7 +895,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
 
     static BaseType_t prvSelectHighestPriorityTask( const BaseType_t xCoreID )
     //@ requires true;
-    //@ assert true;
+    //@ ensures true;
     {
         UBaseType_t uxCurrentPriority = uxTopReadyPriority;
         BaseType_t xTaskScheduled = pdFALSE;
@@ -5353,9 +5353,7 @@ static void prvResetNextTaskUnblockTime( void )
         uint32_t ulState;
 
         ulState = portDISABLE_INTERRUPTS();
-        //@ open coreLocalInterruptInv_p();
         xReturn = pxCurrentTCBs[ portGET_CORE_ID() ];
-        //@ close coreLocalInterruptInv_p();
         portRESTORE_INTERRUPTS( ulState );
 
         return xReturn;
diff --git a/verification/verifast/proof/verifast_port_contracts.h b/verification/verifast/proof/verifast_port_contracts.h
index c2af62d39..77c645b96 100644
--- a/verification/verifast/proof/verifast_port_contracts.h
+++ b/verification/verifast/proof/verifast_port_contracts.h
@@ -35,14 +35,16 @@ uint32_t VF__portDISABLE_INTERRUPTS();
 /*@ ensures result == state &*& 
             interruptState_p(coreID, ?newState) &*&
             interruptsDisabled_f(newState) == true &*&
-            coreLocalInterruptInv_p();
+            interruptsDisabled_f(state) == true
+               ? newState == state 
+               : coreLocalInterruptInv_p();
 @*/
 
 #undef portRESTORE_INTERRUPTS
 #define portRESTORE_INTERRUPTS(ulState) VF__portRESTORE_INTERRUPTS(ulState)
 void VF__portRESTORE_INTERRUPTS(uint32_t ulState);
 /*@ requires interruptState_p(?coreID, ?tmpState) &*&
-             interruptsDisabled_f(tmpState) == true 
+             (interruptsDisabled_f(tmpState) == true && interruptsDisabled_f(ulState) == false)
                 ? coreLocalInterruptInv_p()
                 : true;
  @*/