Fix bug in NAryExpr where is was possible for A.Equals(B) to return

true but A.GetHashCode() == B.GetHashCode() return false.

The case of the bug was that Args.GetHashCode() was being used which
uses Object.GetHashCode() which uses references to compute GetHashCode().
This is wrong because we want hash codes to equal for structural equality.

To fix this I've implemented a really simple hashing method. I have not tested
how resilient this is to collisions.

1 files changed, 5 insertions, 1 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 0a7bfa33..8d372b0c 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -2115,7 +2115,11 @@ namespace Microsoft.Boogie {
     [Pure]

     public override int GetHashCode() {

       int h = this.Fun.GetHashCode();

-      h ^= this.Args.GetHashCode();

+      // DO NOT USE Args.GetHashCode() because that uses Object.GetHashCode() which uses references

+      // We want structural equality

+      foreach (var arg in Args) {

+        h = (97*h) + arg.GetHashCode();

+      }

       return h;

     }

     public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {