diff options
| -rw-r--r-- | Source/Dafny/Triggers/QuantifierSplitter.cs | 10 |
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;
+ }
}
}
}
|