From a1f80cb9e477aba98aef11add502dbeef0670c35 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 29 Jul 2014 14:41:48 +0100 Subject: 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. --- Source/Core/AbsyExpr.cs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'Source/Core/AbsyExpr.cs') 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) { -- cgit v1.2.3