From 0f4f6e8c38ef02fd5761480623d1c16460528727 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 16 Dec 2013 17:46:41 -0800
Subject: Fixed another :never_pattern bug related to nested quantifiers

---
 Test/test2/NeverPattern.bpl | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'Test/test2/NeverPattern.bpl')

diff --git a/Test/test2/NeverPattern.bpl b/Test/test2/NeverPattern.bpl
index 07e4be9c..1e0fed76 100644
--- a/Test/test2/NeverPattern.bpl
+++ b/Test/test2/NeverPattern.bpl
@@ -30,13 +30,13 @@ procedure bar2()
 
 // ----- nested binders -----
 
-function {:never_pattern true} P(int): bool;
+function {:never_pattern} P(int): bool;
 function F(int, int): int;
 function G(int): bool;
 
 procedure NestedBinders()
 {
-  goto A, B, C;
+  goto A, B, C, D;
   A:
     assume (forall s: int ::
       // the occurrence of P in the next line had once caused a crash
@@ -56,5 +56,13 @@ procedure NestedBinders()
       (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:
 }
-- 
cgit v1.2.3