Initial set of files.

1 files changed, 22 insertions, 0 deletions

diff --git a/Test/test20/PolyPolyPoly.bpl b/Test/test20/PolyPolyPoly.bpl
new file mode 100644
index 00000000..8666d1fc
--- /dev/null
+++ b/Test/test20/PolyPolyPoly.bpl
@@ -0,0 +1,22 @@
+

+type C _;

+

+const p: <a>[]a;

+const q: <a>[a, a]a;

+const r: <a>[](C a);

+

+const x: C int;

+const y: C bool;

+

+axiom (p[][:= 5][:= true] == p);

+axiom (p[][:= 5][:= true] == r);               // error

+axiom (p[][:= x][:= y] == p);

+axiom (p[][:= x][:= y] == r);

+axiom (p[][:= x][:= 5] == r);                  // error

+axiom (p[][:= x][:= y] == p[][:= 5][:= true]);

+axiom (q[p[][:= x][:= y], p[][:= 5][:= true]] == p);

+axiom (q[p[], p[]][:= 5][:= true] == p);

+

+axiom (exists<a> x:a :: p[][:= 5][:= true] == x);

+axiom (exists<a,b> x:a, y:b :: p[][:= 5][:= true] == q[x,y]);  // error

+axiom (exists<a,b> x:a, y:b :: q[x, x] == q[y, y]);