From 199b23d8dbadeebbf413905088c55c4de462495c Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 16 Jun 2014 11:25:36 -0700
Subject: Clarified a refinement point in a test file

---
 Test/dafny1/SchorrWaite-stages.dfy | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Test/dafny1')

diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 7b2e7eda..a51a9fd0 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -176,6 +176,7 @@ abstract module M1 refines M0 {
     // discharge the "everything reachable is marked" postcondition, whose proof we postponed above
     // by supplying an assume statement.  Here, we refine that assume statement into an assert.
     assert ...;
+    assume ...;
   }
 }
 
-- 
cgit v1.2.3