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