summaryrefslogtreecommitdiff
path: root/Test/dafny4/Bug68.dfy
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2015-04-14 10:09:03 -0700
committerGravatar qunyanm <unknown>2015-04-14 10:09:03 -0700
commit38134c5587ea53e71290e2e8ea9915062172865b (patch)
tree26116aeedd7ba60a3a3bc91d798d7ea333637d79 /Test/dafny4/Bug68.dfy
parent90c68ad369e3f9318d4f31ed4f9e628cb7f2738d (diff)
Fix issue #68. Change GetHashCode implementation for Sequence.
Diffstat (limited to 'Test/dafny4/Bug68.dfy')
-rw-r--r--Test/dafny4/Bug68.dfy9
1 files changed, 9 insertions, 0 deletions
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