diff options
Diffstat (limited to 'Source/Dafny/Triggers/TriggerExtensions.cs')
-rw-r--r-- | Source/Dafny/Triggers/TriggerExtensions.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 02deb92f..71414eee 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -121,7 +121,7 @@ namespace Microsoft.Dafny.Triggers { }
internal static IEnumerable<TriggerMatch> SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) {
- return quantifier.Term.AllSubExpressions(true, false) //FIXME should loop detection actually pass true here?
+ return quantifier.AllSubExpressions(true, true)
.Select(e => TriggerUtils.PrepareExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e))
.Where(e => e.HasValue).Select(e => e.Value);
}
|