Fixed another :never_pattern bug related to nested quantifiers

2 files changed, 15 insertions, 2 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index b29f60fe..460e786a 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -588,6 +588,11 @@ namespace Microsoft.Boogie {
         }

         return base.VisitNAryExpr(node);

       }

+      public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) {

+        // don't go into quantifier expression or its triggers, since the terms in there may have more bound variables

+        // (note, with only the VisitBinderExpr override below, we'd still be visiting triggers, which we don't want to do)

+        return node;

+      }

       public override BinderExpr VisitBinderExpr(BinderExpr node) {

         // don't go into binder expression, since the terms in there may have more bound variables

         return node;

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:

 }