Made an adjustment in the printing of resolved forall expressions (previous code introduced

with bug fix 103 and tripped over with the /rprint and /autoTriggers:1 flags used in the new
dafny4/UnionFind.dfy test).

1 files changed, 15 insertions, 4 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 0a25b941..6010e2f0 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -846,10 +846,7 @@ namespace Microsoft.Dafny {
         if (attributes == null && s.ForallExpressions != null) {

           foreach (Expression expr in s.ForallExpressions) {

             ForallExpr e = (ForallExpr)expr;

-            while (e != null && attributes == null) {

-              attributes = e.Attributes;

-              e = (ForallExpr)e.SplitQuantifierExpression;

-            }

+            attributes = GetSomeAttributes(e);

             if (attributes != null) { break; }

           }

         }
@@ -1010,6 +1007,20 @@ namespace Microsoft.Dafny {
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
       }
+    }

+

+    private static Attributes GetSomeAttributes(Expression expr) {

+      if (expr is ForallExpr) {

+        var e = (ForallExpr)expr;

+        if (e.Attributes != null) {

+          return e.Attributes;

+        }

+        return GetSomeAttributes(e.SplitQuantifierExpression);

+      } else if (expr is BinaryExpr) {

+        var e = (BinaryExpr)expr;

+        return GetSomeAttributes(e.E0) ?? GetSomeAttributes(e.E1);

+      }

+      return null;

     }
 
     private void PrintModifyStmt(int indent, ModifyStmt s, bool omitFrame) {