Fix issue #67. Check SupportsEquality before determining whether to emit Equals

or == for equality testing.

2 files changed, 18 insertions, 0 deletions

diff --git a/Test/dafny4/Bug67.dfy b/Test/dafny4/Bug67.dfy
new file mode 100644
index 00000000..f1269713
--- /dev/null
+++ b/Test/dafny4/Bug67.dfy
@@ -0,0 +1,11 @@
+// RUN: %dafny /compile:3  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+datatype d = D(m:seq<int>)

+

+method Main()

+{

+  assert D([10, 20]) == D([10, 20]); // succeeds

+  print [10, 20] == [10, 20], "\n"; // prints True

+  print D([10, 20]) == D([10, 20]); // prints False

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug67.dfy.expect b/Test/dafny4/Bug67.dfy.expect
new file mode 100644
index 00000000..d661aac2
--- /dev/null
+++ b/Test/dafny4/Bug67.dfy.expect
@@ -0,0 +1,7 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

+Program compiled successfully

+Running...

+

+True
+True
\ No newline at end of file