From 5b62a70205871f5f4d62db5247f11ac6c53fc57e Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Sat, 22 Aug 2015 15:39:50 -0700
Subject: Look at the full quantifier to find loops, not just the term.

---
 Source/Dafny/Triggers/TriggerExtensions.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source')

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);
     }
-- 
cgit v1.2.3