diff options
| -rw-r--r-- | Source/Core/AbsyType.cs | 2 |
1 files changed, 1 insertions, 1 deletions
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 {
|