Dafny: liberalized equality to work when the types could possibly be the same

(i.e. a != b is allowed when a: array<int> and b: array<T>)

1 files changed, 3 insertions, 3 deletions

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index e56a8317..3e5a95ef 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -11,10 +11,10 @@ class LazyInitArray<T> {
     reads this, a, b, c;

   {

     a != null && b != null && c != null &&

-    a.Length == |Contents| + 1 &&  // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'

+    a.Length == |Contents| &&

     b.Length == |Contents| &&

     c.Length == |Contents| &&

-    b != c &&

+    b != c && a != b && a != c &&

     0 <= n && n <= c.Length &&

     (forall i :: 0 <= i && i < |Contents| ==>

        Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&

@@ -41,7 +41,7 @@ class LazyInitArray<T> {
     ensures |Contents| == N && Zero == zero;

     ensures (forall x :: x in Contents ==> x == zero);

   {

-    a := new T[N+1];

+    a := new T[N];

     b := new int[N];

     c := new int[N];

     n := 0;