summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2016-01-25 11:30:02 -0800
committerGravatar qunyanm <unknown>2016-01-25 11:30:02 -0800
commit436966ef61a3e4330bbe705d0d0319fcde5f3099 (patch)
tree1160382ac78271c1c35fbdc918c40e09447f99ad /Source/Dafny
parent9cf02f9daaba01d48621a932c4984753337fbbc5 (diff)
Fix issue 121. Don't split QuantifierExpr that are empty.
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/Triggers/QuantifierSplitter.cs5
1 files changed, 3 insertions, 2 deletions
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) {