From 8567d68f7f04f87b2d4270e18713bdcdf4d26031 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 10 Feb 2014 18:14:46 -0800
Subject: Fixed errors in the use of Code Contracts

---
 Source/Core/Absy.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/Core/Absy.cs')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index f0e2e7ed..b220b373 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -783,7 +783,7 @@ namespace Microsoft.Boogie {
 
     public static Graph<Block/*!*/>/*!*/ GraphFromImpl(Implementation impl) {
       Contract.Requires(impl != null);
-      Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().TopologicalSort()));
+      Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().Nodes));
       Contract.Ensures(Contract.Result<Graph<Block>>() != null);
 
       Graph<Block/*!*/> g = new Graph<Block/*!*/>();
-- 
cgit v1.2.3