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

the auto-triggers can be computed for ForallStmt.

1 files changed, 1 insertions, 0 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 315b823a..eff7d97d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -235,6 +235,7 @@ namespace Microsoft.Dafny
       rewriters.Add(new AutoReqFunctionRewriter(this.reporter, opaqueRewriter));

       rewriters.Add(opaqueRewriter);

       rewriters.Add(new TimeLimitRewriter(reporter));

+      rewriters.Add(new ForallStmtRewriter(reporter));

 

       if (DafnyOptions.O.AutoTriggers) {

         rewriters.Add(new QuantifierSplittingRewriter(reporter));