Fix autoreq handling of quantifiers

1 files changed, 4 insertions, 1 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 9db7a0ec..53baf8e7 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -950,7 +950,10 @@ namespace Microsoft.Dafny
 

         var auto_reqs = generateAutoReqs(e.Term);

         if (auto_reqs.Count > 0) {

-          reqs.Add(Expression.CreateQuantifier(e, true, andify(e.Term.tok, auto_reqs)));        

+            Expression allReqsSatisfied = andify(e.Term.tok, auto_reqs);

+            Expression allReqsSatisfiedAndTerm = Expression.CreateAnd(allReqsSatisfied, e.Term);

+            e.UpdateTerm(allReqsSatisfiedAndTerm);

+            resolver.ReportAdditionalInformation(e.tok, "autoreq added (" + Printer.ExtendedExprToString(allReqsSatisfied) + ") &&", e.tok.val.Length);

         }

       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;