Merge

2 files changed, 40 insertions, 1 deletions

diff --git a/Test/test2/Answer b/Test/test2/Answer
index e75d69f1..a88587e2 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -308,7 +308,7 @@ NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold.
 Execution trace:

     NeverPattern.bpl(27,3): anon0

 

-Boogie program verifier finished with 1 verified, 3 errors

+Boogie program verifier finished with 2 verified, 3 errors

 

 -------------------- NullaryMaps.bpl --------------------

 NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold.

diff --git a/Test/test2/NeverPattern.bpl b/Test/test2/NeverPattern.bpl
index f0478077..1e0fed76 100644
--- a/Test/test2/NeverPattern.bpl
+++ b/Test/test2/NeverPattern.bpl
@@ -27,3 +27,42 @@ procedure bar2()
   assume (forall x : int :: {:nopats f2(x)} f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3);

   assert f2(3) > 0;

 }

+

+// ----- nested binders -----

+

+function {:never_pattern} P(int): bool;

+function F(int, int): int;

+function G(int): bool;

+

+procedure NestedBinders()

+{

+  goto A, B, C, D;

+  A:

+    assume (forall s: int ::

+      // the occurrence of P in the next line had once caused a crash

+      (forall x: int :: { F(s, x) } P(F(s, x)))

+      ==> G(s));  // this places the nested forall in a negative position

+    goto End;

+

+  B:

+    assume (forall s: int ::

+      // the occurrence of P in the next line had once caused a crash

+      (exists x: int :: { F(s, x) } P(F(s, x))));

+    goto End;

+

+  C:

+    assume (forall s: int, m: [int]bool ::

+      // the occurrence of P in the next line had once caused a crash

+      (lambda x: int :: P(F(s, x))) == m);

+    goto End;

+

+  D:

+    assume (forall x0: int ::

+             // The following quantifier will get a {:nopats P(x1,s)}, which is good.

+             // But that added trigger expression had once caused the outer quantifier

+             // to crash.

+             (forall x1: int :: P(x1)));

+    goto End;

+

+  End:

+}