Initial set of files.

1 files changed, 30 insertions, 0 deletions

diff --git a/Test/test21/DisjointDomains.bpl b/Test/test21/DisjointDomains.bpl
new file mode 100644
index 00000000..88647e6b
--- /dev/null
+++ b/Test/test21/DisjointDomains.bpl
@@ -0,0 +1,30 @@
+type C _;

+

+function f<a>(C a) returns (int);

+

+axiom (forall x : C int :: f(x) == 3);

+axiom (forall x : C bool :: f(x) == 7);

+

+procedure P() returns () {

+  var a : C int, b : C bool, c : C ref;

+

+  start:

+    assert f(a) == 3;

+    assert f(b) == 7;

+    assert f(b) == 8;      // should not be provable

+}

+

+procedure Q() returns () {

+  var c : C ref;

+

+  start:

+    assert f(c) == 7;      // should not be provable

+}

+

+procedure R<a>(c : C a) returns () {

+

+  start:

+    assert f(c) == 7;      // should not be provable

+}

+

+type ref;