Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that

the auto-triggers can be computed for ForallStmt.

1 files changed, 12 insertions, 0 deletions

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index 865aa33e..e46b64fb 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -114,6 +114,18 @@ namespace Microsoft.Dafny.Triggers {
       }

     }

 

+    protected override void VisitOneStmt(Statement stmt) {

+      Contract.Requires(stmt != null);

+      if (stmt is ForallStmt) {

+        ForallStmt s = (ForallStmt)stmt;

+        if (s.ForallExpressions != null) {

+          foreach (Expression expr in s.ForallExpressions) {

+            VisitOneExpr(expr);

+          }

+        }

+      }

+    }

+

     /// <summary>

     /// See comments above definition of splits for reason why this method exists

     /// </summary>