From 5827ea8d4d4771174a864d5425d89bec22d62fa3 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Fri, 19 Feb 2010 22:17:39 +0000
Subject: Fix up the polymorphic case for lambda; it probably still isn't quite
 correct.

---
 Test/test2/Answer         |  6 +++++-
 Test/test2/Lambda.bpl     | 16 ++++++++++++++++
 Test/test2/LambdaPoly.bpl | 18 ++++++++++++++++++
 Test/test2/runtest.bat    |  2 +-
 4 files changed, 40 insertions(+), 2 deletions(-)
 create mode 100644 Test/test2/LambdaPoly.bpl

(limited to 'Test/test2')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 60d76af1..ef808373 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -342,7 +342,11 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Lambda.bpl(36,5): anon0
 
-Boogie program verifier finished with 3 verified, 2 errors
+Boogie program verifier finished with 4 verified, 2 errors
+
+-------------------- LambdaPoly.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
 -------------------- sk_hack.bpl --------------------
 
 Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl
index 48610ff1..177900f4 100644
--- a/Test/test2/Lambda.bpl
+++ b/Test/test2/Lambda.bpl
@@ -38,4 +38,20 @@ procedure fail()
   assert m[1,t] == 2;
 }
 
+type set = [int]bool;
+function union(a:set, b:set) : set;
+axiom (forall a,b:set :: union(a,b) == (lambda x:int :: a[x] || b[x]));
 
+function diff(a:set, b:set) : set {(lambda x:int :: a[x] && !b[x]) }
+
+procedure a()
+{
+  var a:set, b:set;
+  assume a[1];
+  assume b[2];
+  assert union(a,b)[1];
+  assert union(a,b)[2];
+  assume !b[1];
+  assert diff(a,b)[1];
+  assert !diff(a,b)[2];
+}
diff --git a/Test/test2/LambdaPoly.bpl b/Test/test2/LambdaPoly.bpl
new file mode 100644
index 00000000..6d56e7c5
--- /dev/null
+++ b/Test/test2/LambdaPoly.bpl
@@ -0,0 +1,18 @@
+type set a = [a]bool;
+function union<T>(a:set T, b:set T) : set T;
+axiom (forall<T> a,b:set T :: union(a,b) == (lambda x:T :: a[x] || b[x]));
+
+function diff<T>(a:set T, b:set T) : set T {(lambda x:T :: a[x] && !b[x]) }
+
+procedure a()
+{
+  var a:set int, b:set int;
+  assume a[1];
+  assume b[2];
+  assert union(a,b)[1];
+  assert union(a,b)[2];
+  assume !b[1];
+  assert diff(a,b)[1];
+  assert !diff(a,b)[2];
+}
+
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index ea4376b6..f472741c 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -11,7 +11,7 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
             strings-no-where.bpl strings-where.bpl
             Structured.bpl Where.bpl UpdateExpr.bpl
             NeverPattern.bpl NullaryMaps.bpl Implies.bpl
-	    IfThenElse1.bpl Lambda.bpl) do (
+	    IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl) do (
   echo.
   echo -------------------- %%f --------------------
   %BGEXE% %* /noinfer %%f
-- 
cgit v1.2.3