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

1 files changed, 4 insertions, 0 deletions

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

         return base.VisitNAryExpr(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;

+      }

     }

 

     private bool neverTriggerApplied;