Small fix: there is no loop in (forall x :: Q(x) && Q(0))

Again, spotted by Chris :)

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 114d5f5d..b77afccb 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -100,7 +100,9 @@ namespace Microsoft.Dafny.Triggers {
       // quantifier that matches one of the terms of the trigger (this ensures that

       // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even

       // ignore terms that almost match a trigger term, modulo a single variable

-      // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop).

+      // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop). 

+      // The last thing that we ignore is matching variables against constants, 

+      // to ensure that P(x) is not flagged as looping with P(0).

       // This ignoring logic is implemented by the CouldCauseLoops method.

 

       foreach (var q in quantifiers) {