Fix up the polymorphic case for lambda; it probably still isn't quite correct.

4 files changed, 40 insertions, 2 deletions

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