From e3fff39c37ed68cf718eab84613e3bbb02858653 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 20 Aug 2015 10:01:50 -0700
Subject: Allow users to disable quantifier splitting by with a {:split false}
 attribute

---
 Source/Dafny/Triggers/QuantifierSplitter.cs | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index 4b223856..c50bc9c6 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -85,10 +85,12 @@ namespace Microsoft.Dafny.Triggers {
 
     protected override void VisitOneExpr(Expression expr) {
       var quantifier = expr as QuantifierExpr;
-      if (quantifier != null) {
-        var split = SplitQuantifier(quantifier).ToList();
-        quantifier.SplitQuantifier = split;
-        //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));
+      if (quantifier != null && quantifier.SplitQuantifier == null) {
+        bool splitAttr = true;
+        if (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) {
+          var split = SplitQuantifier(quantifier).ToList();
+          quantifier.SplitQuantifier = split;
+        }
       }
     }
   }
-- 
cgit v1.2.3