Allow users to disable quantifier splitting by with a {:split false} attribute

1 files 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;

+        }

       }

     }

   }