From 7fe2ec22f23047649136ec7fbf9fb4aef58f6661 Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Tue, 6 Dec 2022 09:24:08 -0500
Subject: [PATCH] Strengthened postcondition of reordering lemma.

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

diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h
index 549586ff1..c06acf3b6 100644
--- a/verification/verifast/proof/ready_list_predicates.h
+++ b/verification/verifast/proof/ready_list_predicates.h
@@ -285,7 +285,8 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
         readyLists_p(?gReorderedCellLists, ?gReorderedOwnerLists) &*&
         length(gReorderedCellLists) == length(gCellLists) &*&
         length(gReorderedOwnerLists) == length(gOwnerLists) &*&
-        length(gReorderedCellLists) == length(gReorderedOwnerLists);
+        length(gReorderedCellLists) == length(gReorderedOwnerLists) &*&
+        forall(gReorderedOwnerLists, (superset)(gTasks)) == true;
  @*/
 {
     //@ open VF_reordeReadyList__ghost_args(_, _, _, _);