diff options
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 18 | ||||
| -rw-r--r-- | Test/dafny4/Bug68.dfy | 26 | ||||
| -rw-r--r-- | Test/dafny4/Bug68.dfy.expect | 5 |
3 files changed, 40 insertions, 9 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 2a553c81..fd680a0b 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -75,9 +75,9 @@ namespace Dafny return other is Set<T> && Equals((Set<T>)other);
}
public override int GetHashCode() {
- var hashCode = 0;
+ var hashCode = 1;
foreach (var t in dict.Keys) {
- hashCode = (hashCode << 3) | (hashCode >> 29) ^ t.GetHashCode();
+ hashCode = hashCode * (t.GetHashCode()+3);
}
return hashCode;
}
@@ -232,10 +232,11 @@ namespace Dafny return other is MultiSet<T> && Equals((MultiSet<T>)other);
}
public override int GetHashCode() {
- var hashCode = 0;
+ var hashCode = 1;
foreach (var kv in dict) {
- hashCode = (hashCode << 3) | (hashCode >> 29) ^ kv.Key.GetHashCode();
- hashCode = (hashCode << 3) | (hashCode >> 29) ^ kv.Value.GetHashCode();
+ var key = kv.Key.GetHashCode();
+ key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+ hashCode = hashCode * (key + 3);
}
return hashCode;
}
@@ -401,10 +402,11 @@ namespace Dafny return other is Map<U, V> && Equals((Map<U, V>)other);
}
public override int GetHashCode() {
- var hashCode = 0;
+ var hashCode = 1;
foreach (var kv in dict) {
- hashCode = (hashCode << 3) | (hashCode >> 29) ^ kv.Key.GetHashCode();
- hashCode = (hashCode << 3) | (hashCode >> 29) ^ kv.Value.GetHashCode();
+ var key = kv.Key.GetHashCode();
+ key = (key << 3) | (key >> 29) ^ kv.Value.GetHashCode();
+ hashCode = hashCode * (key + 3);
}
return hashCode;
}
diff --git a/Test/dafny4/Bug68.dfy b/Test/dafny4/Bug68.dfy index bfd8c4ad..601da0b2 100644 --- a/Test/dafny4/Bug68.dfy +++ b/Test/dafny4/Bug68.dfy @@ -8,6 +8,14 @@ method M1() print {10, 20} in m, "\n"; // prints False
}
+method M1'()
+{
+ var m := map [{10, 20} := 33];
+ assert {10, 20} == {20, 10};
+ assert {20, 10} in m; // succeeds
+ print {20, 10} in m, "\n"; // prints False
+}
+
method M2()
{
var m := map [(map [1 := 10, 2 := 20]) := 33];
@@ -15,6 +23,14 @@ method M2() print (map [1 := 10, 2 := 20]) in m, "\n"; // prints False
}
+method M2'()
+{
+ var m := map [(map [1 := 10, 2 := 20]) := 33];
+ assert (map [1 := 10, 2 := 20] == map [2 := 20, 1 := 10]);
+ assert (map [2 := 20, 1 := 10]) in m; // succeeds
+ print (map [2 := 20, 1 := 10]) in m, "\n"; // prints False
+}
+
method M3()
{
var m := map [(multiset{10, 20}) := 33];
@@ -22,6 +38,13 @@ method M3() print (multiset{10, 20}) in m, "\n"; // prints False
}
+method M3'()
+{
+ var m := map [(multiset{10, 20}) := 33];
+ assert multiset{10, 20} == multiset{20, 10};
+ assert (multiset{20, 10}) in m; // succeeds
+ print (multiset{20, 10}) in m, "\n"; // prints False
+}
method M4()
{
@@ -33,7 +56,10 @@ method M4() method Main()
{
M1();
+ M1'();
M2();
+ M2'();
M3();
+ M3'();
M4();
}
\ No newline at end of file diff --git a/Test/dafny4/Bug68.dfy.expect b/Test/dafny4/Bug68.dfy.expect index 22cf7e4d..98b1498e 100644 --- a/Test/dafny4/Bug68.dfy.expect +++ b/Test/dafny4/Bug68.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 10 verified, 0 errors
+Dafny program verifier finished with 16 verified, 0 errors
Program compiled successfully
Running...
@@ -7,3 +7,6 @@ True True True True +True +True +True |