From 436966ef61a3e4330bbe705d0d0319fcde5f3099 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Mon, 25 Jan 2016 11:30:02 -0800
Subject: Fix issue 121. Don't split QuantifierExpr that are empty.

---
 Source/Dafny/Triggers/QuantifierSplitter.cs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
index d0b2b430..b039a402 100644
--- a/Source/Dafny/Triggers/QuantifierSplitter.cs
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -100,8 +100,9 @@ namespace Microsoft.Dafny.Triggers {
     }
     
     private static bool AllowsSplitting(QuantifierExpr quantifier) {
-      bool splitAttr = true;
-      return !Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr;
+      // allow split if attributes doesn't contains "split" or it is "split: true" and it is not an empty QuantifierExpr (boundvar.count>0)
+      bool splitAttr = true; 
+      return (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) && (quantifier.BoundVars.Count > 0);
     }
 
     protected override void VisitOneExpr(Expression expr) {
-- 
cgit v1.2.3