diff options
| -rw-r--r-- | Test/civl/ticket.bpl | 2 |
1 files changed, 1 insertions, 1 deletions
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; }|; |