diff options
| author |  qadeer <unknown> | 2013-12-22 00:34:35 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-12-22 00:34:35 -0800 |
| commit | 9decee118ad579769bea68c2542162b1aed7d440 (patch) | |
| tree | b88316f3b7a1213e10fe67a18c73c5a9f27f4031 /Test/og/ticket.bpl | |
| parent | ca02664886e23e4d26e9a19b07c51b82de9d9e4f (diff) | |
bug fixes in Duplicate.cs and parsing of invariant attributes
other bug fixes in QED stuff
Diffstat (limited to 'Test/og/ticket.bpl')
| -rw-r--r-- | Test/og/ticket.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index 9f467229..b628df30 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -1,5 +1,7 @@ function RightOpen(n: int) : [int]bool;
function RightClosed(n: int) : [int]bool;
+axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
+axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
|