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 | 4ccc3c70255b59a835b099e962ba1d011696a682 (patch) | |
| tree | 7333d39696c061eeaf2238ec20ffce379b278421 /DafnyDriver | |
| parent | 5174c7f2f12f3ecb5c9c050bf331756c3f757048 (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 'DafnyDriver')
| -rw-r--r-- | DafnyDriver/DafnyDriver.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 3fa678a8..5e227011 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/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");
}
}
|