Further relax the loop detection conditions

Mismatches are now allowed up to expressions not involving any of the bound
variables of the quantifier under inspection.

1 files changed, 2 insertions, 1 deletions

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index d78bcb9e..cc3b1978 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -69,7 +69,8 @@ namespace Microsoft.Dafny.Triggers {
     internal IEnumerable<TriggerMatch> LoopingSubterms(QuantifierExpr quantifier) {

       Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       var matchingSubterms = this.MatchingSubterms(quantifier);

-      return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms));

+      var boundVars = new HashSet<BoundVar>(quantifier.BoundVars);

+      return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars));

     }

 

     internal List<TriggerMatch> MatchingSubterms(QuantifierExpr quantifier) {