diff options
| author |  qadeer <unknown> | 2014-02-12 10:06:54 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-02-12 10:06:54 -0800 |
| commit | 5ad109ceffd8bf8c671e3605ac7530c8448b38b6 (patch) | |
| tree | 4b3d84266416cce21558541d1641eadb52e25f5c /Test/og/civl-paper.bpl | |
| parent | be5d4b874eac8d6b17bb39728f5f5c30790a28cc (diff) | |
fixed the civl-paper example
Diffstat (limited to 'Test/og/civl-paper.bpl')
| -rw-r--r-- | Test/og/civl-paper.bpl | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl index fbe8ef59..4ebaadbe 100644 --- a/Test/og/civl-paper.bpl +++ b/Test/og/civl-paper.bpl @@ -1,6 +1,12 @@ type X;
const nil: X;
+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
+{
+ MapConstBool(false)[x := true]
+}
+
type lmap;
function {:linear "mem"} dom(lmap): [int]bool;
function map(lmap): [int]int;
|