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