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

1 files changed, 18 insertions, 0 deletions

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];
+}
+