Fixed bug in never_pattern functionality. In the new design, never_pattern does not assemble any nopats from nested quantifiers/lambdas.

1 files changed, 31 insertions, 0 deletions

diff --git a/Test/test2/NeverPattern.bpl b/Test/test2/NeverPattern.bpl
index f0478077..07e4be9c 100644
--- a/Test/test2/NeverPattern.bpl
+++ b/Test/test2/NeverPattern.bpl
@@ -27,3 +27,34 @@ 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 true} P(int): bool;

+function F(int, int): int;

+function G(int): bool;

+

+procedure NestedBinders()

+{

+  goto A, B, C;

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

+

+  End:

+}