From f367cffd4cdc9f6b7c626117f986e9c7a73d44b6 Mon Sep 17 00:00:00 2001
From: nisarg-certora <nisarg@certora.com>
Date: Tue, 12 Nov 2024 14:11:25 -0500
Subject: [PATCH] fix: peterson create spec

---
 test/comparison/peterson.rav | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test/comparison/peterson.rav b/test/comparison/peterson.rav
index 2bcbf58..29530ca 100644
--- a/test/comparison/peterson.rav
+++ b/test/comparison/peterson.rav
@@ -44,7 +44,9 @@ module Peterson[R: LockResource]
         returns (l: Ref)
         requires resource(r)
         ensures peterson_inv(l, r)
+        ensures own(l.wait_left, false, 0.5)
         ensures own(l.active_left, false, 0.5)
+        ensures own(l.wait_right, false, 0.5)
         ensures own(l.active_right, false, 0.5)
     {
         l := new(