From 2c93b838927128721698eba02c146af4e716ce4d Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 8 Jul 2014 13:47:08 -0700
Subject: Cleaned up a test program

---
 Test/vstte2012/RingBufferAuto.dfy | 2 --
 1 file changed, 2 deletions(-)

(limited to 'Test/vstte2012')

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];
-- 
cgit v1.2.3