1 files changed, 7 insertions, 3 deletions
diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
index a43aae7a..b30cb6b1 100644
--- a/Source/Dafny/Triggers/QuantifiersCollector.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -9,6 +9,7 @@ using System.Diagnostics.Contracts;
 namespace Microsoft.Dafny.Triggers { //FIXME rename this file
   internal class QuantifierCollector : TopDownVisitor<object> {
     readonly ErrorReporter reporter;
+    private HashSet<Expression> quantifiers = new HashSet<Expression>();
     internal List<QuantifiersCollection> quantifierCollections = new List<QuantifiersCollection>();
 
     public QuantifierCollector(ErrorReporter reporter) {
@@ -16,17 +17,20 @@ namespace Microsoft.Dafny.Triggers { //FIXME rename this file
       this.reporter = reporter;
     }
 
-    protected override bool VisitOneExpr(Expression expr, ref object st) {
+    protected override bool VisitOneExpr(Expression expr, ref object _) {
       var quantifier = expr as QuantifierExpr;
-      if (quantifier != null) {
+
+      if (quantifier != null && !quantifiers.Contains(quantifier)) {
+        quantifiers.Add(quantifier);
         if (quantifier.SplitQuantifier != null) {
           var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null);
           quantifierCollections.Add(new QuantifiersCollection(collection, reporter));
-          return false;
+          foreach (var q in quantifier.SplitQuantifier) { quantifiers.Add(q); }
         } else {
           quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));
         }
       }
+
       return true;
     }
   }