diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-09 19:22:07 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-09 19:22:07 -0800 |
| commit | 37b7f425279bb9fe9ce7b14675932eb6702e1450 (patch) | |
| tree | b5a9052777d52eea19ddd6c06dfe4e456f0309d5 /Source/DafnyDriver/DafnyDriver.cs | |
| parent | c28d01d5ee225caaf50d657a1edd7b3211899d84 (diff) | |
Dafny: changed translation to be sensitive to refinement inheritance; this feature is now functional, provided the refining module does not add or change anything
Diffstat (limited to 'Source/DafnyDriver/DafnyDriver.cs')
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 3fa678a8..5e227011 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -638,7 +638,8 @@ namespace Microsoft.Dafny {
if (CommandLineOptions.Clo.Trace)
{
- timeIndication = string.Format(" [{0} s, {1} proof obligations] ", elapsed.TotalSeconds, vcgen.CumulativeAssertionCount - prevAssertionCount);
+ int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;
+ timeIndication = string.Format(" [{0} s, {1} proof obligation{2}] ", elapsed.TotalSeconds, poCount, poCount == 1 ? "" : "s");
}
}
|