Reverted some accidental changes to a test case

1 files changed, 2 insertions, 11 deletions

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index 73a6c3fd..f51a36b2 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -43,18 +43,9 @@ class {:autocontracts} RingBuffer<T>
   }

 

   method Enqueue(x: T)

-    //requires |Contents| != N;

-    ensures Contents == old(Contents) + [x] && N >= old(N);

+    requires |Contents| != N;

+    ensures Contents == old(Contents) + [x] && N == old(N);

   {

-    if (len == data.Length) {

-      var more := data.Length;

-      var d := new T[data.Length + more];

-      parallel (i | 0 <= i < data.Length) {

-        d[if i < start then i else i + more] := data[i];

-      }

-      data := d;

-      N, start := N + more, start + more;

-    }

     var nextEmpty := if start + len < data.Length 

                      then start + len else start + len - data.Length;

     data[nextEmpty] := x;