diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2014-07-28 16:32:51 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-07-28 16:32:51 +0100 |
| commit | cbabeb3fdef4f1ad2aed7f32ba375ad4fdd6c298 (patch) | |
| tree | ce6c80d6383113446e8bb44bd10fa02e0b7fbcb5 /Source/Core/AbsyExpr.cs | |
| parent | 5c5ece158229ad33f36afed8af3b5e47d99987f1 (diff) | |
Fix bug in NAryExpr where Equals() override was not correctly implemented.
The previous implementation which called object.Equals(this.Args, other.Args)
would in turn call ``this.Args.Equals(others.Args)`` which for List<> is
reference equality. Equals() is purposely overloaded on Expr classes in Boogie
to provide structural equality so this has been fixed so a comparision of
elements in the list is performed.
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index bc603ea5..0a7bfa33 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -2110,7 +2110,7 @@ namespace Microsoft.Boogie { return false;
NAryExpr other = (NAryExpr)obj;
- return object.Equals(this.Fun, other.Fun) && object.Equals(this.Args, other.Args);
+ return object.Equals(this.Fun, other.Fun) && this.Args.SequenceEqual(other.Args);
}
[Pure]
public override int GetHashCode() {
|