small update to the example

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 316c09c6..fe56fb27 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -11,12 +11,12 @@ var {:qed} s: int;
 var {:qed} cs: X;

 var {:qed} T: [int]bool;

 

-function Inv1(tickets: [int]bool, ticket: int): (bool)

+function {:inline} Inv1(tickets: [int]bool, ticket: int): (bool)

 {

     tickets == RightOpen(ticket)

 }

 

-function Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)

+function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)

 {

     if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket)

 }