From 8131e68401d9f97d1216be32f3d0e23db83da744 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Sat, 28 Nov 2015 22:22:52 -0800
Subject: 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).

---
 Source/Dafny/Printer.cs | 19 +++++++++++++++----
 1 file 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) {
-- 
cgit v1.2.3