From 1005adb004baf133b265eda5bfdc53022437e6ef Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 23 Jan 2013 18:13:36 -0800
Subject: Fixed bug in translation of method termination checks, and also fixed
 a (previously undetected) specification bug in the test suite.

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

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index 405f3e15..a16cf603 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -83,7 +83,7 @@ class ExtensibleArray<T> {
     modifies Repr;
     ensures Valid() && fresh(Repr - old(Repr));
     ensures Contents == old(Contents) + [t];
-    decreases Repr;
+    decreases Contents;
   {
     if (length == 0 || length % 256 != 0) {
       // there is room in "elements"
-- 
cgit v1.2.3