summaryrefslogtreecommitdiff
path: root/Source/Dafny/Triggers
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-22 15:39:50 -0700
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2015-08-22 15:39:50 -0700
commit5b62a70205871f5f4d62db5247f11ac6c53fc57e (patch)
treeaa40fed98694e0ffca68f48a5021dcc821441b2b /Source/Dafny/Triggers
parent109a5ba2678d911eaa4446674988101677096896 (diff)
Look at the full quantifier to find loops, not just the term.
Diffstat (limited to 'Source/Dafny/Triggers')
-rw-r--r--Source/Dafny/Triggers/TriggerExtensions.cs2
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);
}