From feb7e707b9676ddc076e2e1cae5de884d29ac013 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 15 Apr 2014 17:22:31 -0700
Subject: Fixed malformed Contracts section

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

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

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 00e1a5c6..a1240c30 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -2093,12 +2093,12 @@ Contract.Requires(that != null);
     private static int MinBitsFor(Type t) {
       Contract.Requires(t != null);
       Contract.Requires(t.IsBv);
+      Contract.Ensures(0 <= Contract.Result<int>());
 
       if (t is TypeSynonymAnnotation) {
         return MinBitsFor(((TypeSynonymAnnotation)t).ExpandedType);
       }
 
-      Contract.Ensures(0 <= Contract.Result<int>());
       if (t is BvType) {
         return t.BvBits;
       } else {
-- 
cgit v1.2.3