diff options
Diffstat (limited to 'Source/Dafny/Triggers/TriggerUtils.cs')
| -rw-r--r-- | Source/Dafny/Triggers/TriggerUtils.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index dedbcbb1..6c6eede2 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -101,6 +101,7 @@ namespace Microsoft.Dafny.Triggers { }
internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) {
+ Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier
return quantifier.Attributes.AsEnumerable().All(aa => aa.Name != "trigger" && aa.Name != "no_trigger");
}
}
|