diff options
| author |  wuestholz <unknown> | 2013-06-20 14:28:09 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-20 14:28:09 -0700 |
| commit | 5d1b6d2b134d05311380abb444c04031a263b7f6 (patch) | |
| tree | 923b4f98ef1fc0c364f80d514292038d2d5f0625 /Source/DafnyDriver | |
| parent | 2a8f3ffca06ab037ba8f0eda29072337b7775af1 (diff) | |
Fixed a contract.
Diffstat (limited to 'Source/DafnyDriver')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 89a01ea9..5685528c 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -160,7 +160,7 @@ namespace Microsoft.Dafny {
Contract.Requires(program != null);
Contract.Requires(bplFileName != null);
- Contract.Ensures(0 <= Contract.ValueAtReturn(out stats.InconclusiveCount) && 0 <= Contract.ValueAtReturn(out stats.TimeoutCount));
+ Contract.Ensures(0 <= Contract.ValueAtReturn(out stats).InconclusiveCount && 0 <= Contract.ValueAtReturn(out stats).TimeoutCount);
stats = new PipelineStatistics();
PipelineOutcome oc = ExecutionEngine.ResolveAndTypecheck(program, bplFileName);
|