1 files changed, 55 insertions, 0 deletions
diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy
new file mode 100644
index 00000000..3dc52c80
--- /dev/null
+++ b/Test/dafny0/LiberalEquality.dfy
@@ -0,0 +1,55 @@
+
+class Array<T>
+{
+   var Length: nat;
+}
+
+class Test<T> {
+  var a: Array<int>;
+  var b: Array<T>;
+  predicate valid()
+      reads this, a, b;
+  {
+      a != null && b != null && a != b && a.Length == b.Length
+  }
+}
+
+method m1<T, U>(t: T, u: U)
+   requires t != u;
+{
+   
+}
+
+method m2<T>(t: array<T>, a: array<int>)
+   requires t != null && a != null && t != a && t.Length == a.Length;
+{
+
+}
+
+
+class Weird<T, U, V>
+{
+
+}
+
+
+method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)
+   requires a == b; // Bad: second parameter can't be both bool and int.
+{
+
+}
+
+
+method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)
+  requires a == b;
+{
+
+}
+
+
+// Just to make sure nothing went wrong.
+method m5(a: array<int>, b: array<bool>)
+   requires a == b; // Bad: never equal
+{
+
+}