From b8fad094ad74180ca16670bebe602737d856b5da Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Wed, 25 Nov 2015 10:27:02 -0800
Subject: Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger
 so that the auto-triggers can be computed for ForallStmt.

---
 Source/Dafny/Triggers/QuantifierSplitter.cs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs')

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>
-- 
cgit v1.2.3