Fix bug in BinderExpr where Equals() was not corrected implemented.

BinderExpr was doing:

object.Equals(this.TypeParameters, other.TypeParameters)
&& object.Equals(this.Dummies, other.Dummies)

Both of these are wrong because these are of type List<> and so

- object.Equals(this.TypeParamters, other.TypeParameters) will call this.TypeParameters.Equals(other.TypeParamters) (assuming they aren't references to the same list)
- object.Equals(this.Dummies, other.TypeParameters) will call this.TypeParameters.Equals(other.Dummies) (assuming they aren't references to the same list)

so this is becomes a reference comparision on Lists<>. This is wrong
because Equals() has been overloaded to implement structural equality.

This affects the classes ForallExpr, LambdaExpr and ExistsExpr.

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index c9e8f210..ce591cee 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -88,8 +88,8 @@ namespace Microsoft.Boogie {
 

       BinderExpr other = (BinderExpr)obj;

       // Note, we consider quantifiers equal modulo the Triggers.

-      return object.Equals(this.TypeParameters, other.TypeParameters)

-             && object.Equals(this.Dummies, other.Dummies)

+      return this.TypeParameters.SequenceEqual(other.TypeParameters)

+             && this.Dummies.SequenceEqual(other.Dummies)

              && object.Equals(this.Body, other.Body);

     }