From 9cf02f9daaba01d48621a932c4984753337fbbc5 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Mon, 25 Jan 2016 11:27:26 -0800
Subject: Fix issue 122. Only generate autoTriggers for QuantifierExpr that are
 not empty.

---
 Source/Dafny/Triggers/QuantifiersCollector.cs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Source')

diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
index b887435b..cb2d5c6d 100644
--- a/Source/Dafny/Triggers/QuantifiersCollector.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -21,7 +21,8 @@ namespace Microsoft.Dafny.Triggers {
     protected override bool VisitOneExpr(Expression expr, ref bool inOldContext) {
       var quantifier = expr as QuantifierExpr;
 
-      if (quantifier != null && !quantifiers.Contains(quantifier)) {
+      // only consider quantifiers that are not empty (Bound.Vars.Count > 0)
+      if (quantifier != null && (quantifier.BoundVars.Count > 0) && !quantifiers.Contains(quantifier)) {
         quantifiers.Add(quantifier);
         if (quantifier.SplitQuantifier != null) {
           var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null);
-- 
cgit v1.2.3