Fixed another :never_pattern bug related to nested quantifiers

1 files changed, 10 insertions, 2 deletions

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:

 }