Add alpha equivalence check for Expr, and use it when lambda lifting

1 files changed, 14 insertions, 2 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index bc603ea5..7e71453b 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1893,7 +1893,19 @@ namespace Microsoft.Boogie {
       this.Type = type;

     }

 

-    public string/*!*/ FunctionName {

+    public override bool Equals(object obj) {

+      TypeCoercion other = obj as TypeCoercion;

+      if (other == null) {

+        return false;

+      } else {

+        return object.Equals(Type, other.Type);

+      }

+    }

+

+

+

+    public

+      string/*!*/ FunctionName {

       get {

         Contract.Ensures(Contract.Result<string>() != null);

 

@@ -2110,7 +2122,7 @@ namespace Microsoft.Boogie {
         return false;

 

       NAryExpr other = (NAryExpr)obj;

-      return object.Equals(this.Fun, other.Fun) && object.Equals(this.Args, other.Args);

+      return this.Args.ListEquals(other.Args) && object.Equals(this.Fun, other.Fun); 

     }

     [Pure]

     public override int GetHashCode() {