diff options
| author |  wuestholz <unknown> | 2013-12-11 18:30:07 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-12-11 18:30:07 +0100 |
| commit | 9ee988513091d620555874b8a8c82c152b342844 (patch) | |
| tree | 62c6405079d1bb7b99f9f790dbc78e36aad6d351 /Source | |
| parent | 8f143f70ce8a013f0273c885c184b5f96432943a (diff) | |
Remove some (redundant) preconditions to avoid 'ccrewrite' errors.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Inline.cs | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index ad9ecef0..09352900 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -281,9 +281,6 @@ namespace Microsoft.Boogie { public virtual List<Block/*!*/>/*!*/ DoInlineBlocks(List<Block/*!*/>/*!*/ blocks, ref bool inlinedSomething) {
Contract.Requires(cce.NonNullElements(blocks));
- Contract.Requires(program != null);
- Contract.Requires(newLocalVars != null);
- Contract.Requires(newModifies != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
List<Block/*!*/>/*!*/ newBlocks = new List<Block/*!*/>();
|