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 ++-
 Test/dafny4/Bug122.dfy                        | 17 +++++++++++++++++
 Test/dafny4/Bug122.dfy.expect                 |  2 ++
 3 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny4/Bug122.dfy
 create mode 100644 Test/dafny4/Bug122.dfy.expect

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);
diff --git a/Test/dafny4/Bug122.dfy b/Test/dafny4/Bug122.dfy
new file mode 100644
index 00000000..adbee30d
--- /dev/null
+++ b/Test/dafny4/Bug122.dfy
@@ -0,0 +1,17 @@
+// RUN: %dafny /compile:0 /autoTriggers:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Try (a:int) 
+{
+	forall
+    ensures a == a;
+	{
+	}
+} 
+
+
+
+
+
+
+
diff --git a/Test/dafny4/Bug122.dfy.expect b/Test/dafny4/Bug122.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/dafny4/Bug122.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
-- 
cgit v1.2.3