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;