From 0632d3956b7cd10cdc4975cdfc669b73892a121d Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Tue, 19 Jul 2016 05:38:30 -0700 Subject: update --- Test/civl/ticket.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/civl/ticket.bpl b/Test/civl/ticket.bpl index 7db23dca..2e0c6cd1 100644 --- a/Test/civl/ticket.bpl +++ b/Test/civl/ticket.bpl @@ -151,7 +151,7 @@ procedure {:yields} {:layer 0,2} WaitAndEnter({:linear "tid"} tid: X, m:int); ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|; procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X); -ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|; +ensures {:atomic} |{ A: assert cs == tid; s := s + 1; cs := nil; return true; }|; procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); ensures {:atomic} |{ A: assume xl != nil; return true; }|; -- cgit v1.2.3