diff options
| author |  Rustan Leino <unknown> | 2014-04-15 17:22:31 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-15 17:22:31 -0700 |
| commit | feb7e707b9676ddc076e2e1cae5de884d29ac013 (patch) | |
| tree | 36b52a1abe74e9a7203e69d92cf0d264ba2ef0c9 /Source/Core/AbsyType.cs | |
| parent | 2b2d7c7f4ec6226c54ad664ce390fefdaf8fecaf (diff) | |
Fixed malformed Contracts section
Diffstat (limited to 'Source/Core/AbsyType.cs')
| -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 {
|