From d746a27233a460714bcc04fe8e80a765279046be Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Fri, 11 Nov 2022 15:07:01 -0500
Subject: [PATCH] Added missing task-ISR lock invariant to post condition of
 acquision lemma.

---
 verification/verifast/proof/verifast_lock_predicates.h | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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();
 @*/