From 04c8cca7653c2952df11ada7ecd39069388fa5f1 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 23 Jan 2013 18:20:15 -0800
Subject: Fixed another specification bug in a test case.

---
 Test/dafny1/ExtensibleArrayAuto.dfy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
index 3e91fa4b..a3c5593c 100644
--- a/Test/dafny1/ExtensibleArrayAuto.dfy
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -70,7 +70,7 @@ class {:autocontracts} ExtensibleArray<T> {
 
   method Append(t: T)
     ensures Contents == old(Contents) + [t];
-    decreases Repr;
+    decreases Contents;
   {
     if (length == 0 || length % 256 != 0) {
       // there is room in "elements"
-- 
cgit v1.2.3