summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-01-09 11:50:38 -0800
committerGravatar qadeer <unknown>2014-01-09 11:50:38 -0800
commitdacceb34da85edf3f48ab25e06b1e42ffea06c38 (patch)
tree1fdce5d6583a1a84d8f584f7ee9aebca3405bf8f /Test
parent59732afd306a62d53143c2e627fadb97fc0ee9c8 (diff)
small update to the example
Diffstat (limited to 'Test')
-rw-r--r--Test/og/ticket.bpl4
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)
}