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

the auto-triggers can be computed for ForallStmt.

1 files changed, 13 insertions, 0 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
index 1f37dcfa..789e7614 100644
--- a/Source/Dafny/Triggers/QuantifiersCollector.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -40,5 +40,18 @@ namespace Microsoft.Dafny.Triggers {
 

       return true;

     }

+

+    protected override bool VisitOneStmt(Statement stmt, ref bool st) {

+      Contract.Requires(stmt != null);

+      if (stmt is ForallStmt) {

+        ForallStmt s = (ForallStmt)stmt;

+        if (s.ForallExpressions != null) {

+          foreach (Expression expr in s.ForallExpressions) {

+            VisitOneExpr(expr, ref st);

+          }

+        }

+      }

+      return true;

+    }

   }

 }