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

3 files changed, 36 insertions, 1 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;

diff --git a/Test/test2/Answer b/Test/test2/Answer
index e75d69f1..a88587e2 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -308,7 +308,7 @@ NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold.
 Execution trace:

     NeverPattern.bpl(27,3): anon0

 

-Boogie program verifier finished with 1 verified, 3 errors

+Boogie program verifier finished with 2 verified, 3 errors

 

 -------------------- NullaryMaps.bpl --------------------

 NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold.

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:

+}