diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h
index 454a644c7..57d1fd1e9 100644
--- a/verification/verifast/proof/verifast_lock_predicates.h
+++ b/verification/verifast/proof/verifast_lock_predicates.h
@@ -126,7 +126,8 @@ requires locked(?heldLocks) &*&
          heldLocks == cons(?i, cons(?t, nil)) &*&
          i == pair(?f_isr, isrLockID_f()) &*&
          t == pair(?f_task, taskLockID_f());
-ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) );
+ensures locked( cons( pair(_, taskISRLockID_f()), heldLocks) ) &*&
+        taskISRLockInv();
 @*/