Improve the redundancy detection algorithm used while constructing sets of terms

Based on an issue noted by Chris with redundancy removal resuls being dependent
on the order of the terms. Interestingly, one of our tests already had an
instance of that problem.

Also fix the issue with nested quantifiers getting redundant triggers.

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 69c47d90..d78bcb9e 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -11,6 +11,11 @@ namespace Microsoft.Dafny.Triggers {
     internal Expression Expr { get; set; }

     internal Expression OriginalExpr { get; set; }

     internal ISet<IVariable> Variables { get; set; }

+    internal IEnumerable<BoundVar> BoundVars {

+      get {

+        return Variables.Select(v => v as BoundVar).Where(v => v != null);

+      }

+    }

 

     public override string ToString() {

       return Printer.ExprToString(Expr);