Initial set of files.

1 files changed, 27 insertions, 0 deletions

diff --git a/Test/test21/InterestingExamples3.bpl b/Test/test21/InterestingExamples3.bpl
new file mode 100644
index 00000000..8eef3dff
--- /dev/null
+++ b/Test/test21/InterestingExamples3.bpl
@@ -0,0 +1,27 @@
+

+procedure P() returns () {

+

+ assume (forall<t> m : [t]bool ::                // uses "infinitely many" map types

+         (forall x : t ::    m[x] == false));

+

+}

+

+

+procedure Q() returns () {

+ var h : [int] bool;

+

+ assume (forall<t> m : [t]bool, x : t ::    m[x] == false);

+ assert !h[42];

+ assert false;                    // should really be provable

+}

+

+

+

+procedure R() returns () {

+ var h : [int] bool;

+

+ assume (forall<t> m : [t]bool, x : t ::    m[x] == false);

+ assert !h[42];

+ assert !h[42 := true][42];

+ assert false;                    // wow

+}