summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2014-02-12 10:06:54 -0800
committerGravatar qadeer <unknown>2014-02-12 10:06:54 -0800
commit5ad109ceffd8bf8c671e3605ac7530c8448b38b6 (patch)
tree4b3d84266416cce21558541d1641eadb52e25f5c /Test
parentbe5d4b874eac8d6b17bb39728f5f5c30790a28cc (diff)
fixed the civl-paper example
Diffstat (limited to 'Test')
-rw-r--r--Test/og/civl-paper.bpl6
-rw-r--r--Test/og/runtest.bat2
2 files changed, 7 insertions, 1 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;
diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index b5802aa5..80f614ae 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (
%BGEXE% %* /nologo /noinfer %%f
)
-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl DeviceCache.bpl ticket.bpl lock.bpl lock2.bpl multiset.bpl) do (
+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl DeviceCache.bpl ticket.bpl lock.bpl lock2.bpl multiset.bpl civl-paper.bpl) do (
echo.
echo -------------------- %%f --------------------
%BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f