From 927a76b4b1461ac549bc12f24c7bf73f610bd4e4 Mon Sep 17 00:00:00 2001
From: Unknown <namin@idea>
Date: Wed, 26 Jun 2013 17:48:12 -0700
Subject: Changed ranking function for Seq, so that it's compatible with data
 types.

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

(limited to 'Test/vstte2012')

diff --git a/Test/vstte2012/RingBufferAuto.dfy b/Test/vstte2012/RingBufferAuto.dfy
index f51a36b2..7ce48fcc 100644
--- a/Test/vstte2012/RingBufferAuto.dfy
+++ b/Test/vstte2012/RingBufferAuto.dfy
@@ -55,6 +55,8 @@ 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];
-- 
cgit v1.2.3