From 38134c5587ea53e71290e2e8ea9915062172865b Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Tue, 14 Apr 2015 10:09:03 -0700
Subject: Fix issue #68. Change GetHashCode implementation for Sequence.

---
 Binaries/DafnyRuntime.cs     | 8 +++++++-
 Test/dafny4/Bug68.dfy        | 9 +++++++++
 Test/dafny4/Bug68.dfy.expect | 6 ++++++
 3 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny4/Bug68.dfy
 create mode 100644 Test/dafny4/Bug68.dfy.expect

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index ef6da67e..a682422a 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -499,7 +499,13 @@ namespace Dafny
       return other is Sequence<T> && Equals((Sequence<T>)other);
     }
     public override int GetHashCode() {
-      return elmts.GetHashCode();
+      if (elmts == null || elmts.Length == 0)
+        return 0;
+      var hashCode = 0;
+      for (var i = 0; i < elmts.Length; i++) {
+        hashCode = (hashCode << 3) | (hashCode >> 29) ^ elmts[i].GetHashCode();
+      }
+      return hashCode;
     }
     public override string ToString() {
       if (elmts is char[]) {
diff --git a/Test/dafny4/Bug68.dfy b/Test/dafny4/Bug68.dfy
new file mode 100644
index 00000000..2736246d
--- /dev/null
+++ b/Test/dafny4/Bug68.dfy
@@ -0,0 +1,9 @@
+// RUN: %dafny /compile:3  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main()
+{
+  var m := map [[10, 20] := 33];
+  assert [10, 20] in m; // succeeds 
+  print [10, 20] in m; // prints False
+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug68.dfy.expect b/Test/dafny4/Bug68.dfy.expect
new file mode 100644
index 00000000..4fcef38e
--- /dev/null
+++ b/Test/dafny4/Bug68.dfy.expect
@@ -0,0 +1,6 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
+Program compiled successfully
+Running...
+
+True
\ No newline at end of file
-- 
cgit v1.2.3