Initial set of files.

1 files changed, 19 insertions, 0 deletions

diff --git a/Test/test21/HeapAbstraction.bpl b/Test/test21/HeapAbstraction.bpl
new file mode 100644
index 00000000..1d2a7f99
--- /dev/null
+++ b/Test/test21/HeapAbstraction.bpl
@@ -0,0 +1,19 @@
+

+

+type Field a, Heap = <a>[ref, Field a]a;

+

+function f<b>(<a>[b, Field a]a) returns (int);

+

+axiom (forall x:<a>[int, Field a]a :: f(x) == 17);

+

+axiom (forall x:<a>[ref, Field a]a :: f(x) == 42);

+

+procedure P() returns () {

+  var h : Heap, g : <a>[bool, Field a]a;

+

+  assert f(h) == 42;

+  assert f(g) >= 0;     // should not be provable

+}

+

+type ref;

+const null : ref;