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/BoogieDriver | |
| 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/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 4ec10162..32c3b194 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -588,7 +588,8 @@ namespace Microsoft.Boogie { TimeSpan elapsed = end - start;
if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {
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");
}
}
|