From 5ad109ceffd8bf8c671e3605ac7530c8448b38b6 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 12 Feb 2014 10:06:54 -0800 Subject: fixed the civl-paper example --- Test/og/civl-paper.bpl | 6 ++++++ Test/og/runtest.bat | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) 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 -- cgit v1.2.3