Cleaned up a test program

1 files changed, 0 insertions, 2 deletions

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index a4bdf0a0..142d0279 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -76,8 +76,6 @@ class {:autocontracts} RingBuffer<T>
 

   method Dequeue() returns (x: T)

     requires Contents != [];

-    modifies Repr;

-    ensures Valid() && fresh(Repr - old(Repr));

     ensures x == old(Contents)[0] && Contents == old(Contents)[1..] && N == old(N);

   {

     x := data[start];  assert x == Contents[0];