Skip to content

Commit a30ee22

Browse files
atombcpitclaudel
authored andcommitted
Sort output of /verificationLogger:text
The order of elements in the lists it iterates over can vary when using multiple cores.
1 parent ee8c6bb commit a30ee22

File tree

1 file changed

+5
-3
lines changed

1 file changed

+5
-3
lines changed

Source/DafnyDriver/TextLogger.cs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
using System;
22
using System.Collections.Generic;
33
using System.IO;
4+
using System.Linq;
45
using Microsoft.Boogie;
56

67
namespace Microsoft.Dafny;
@@ -13,13 +14,14 @@ public void Initialize(Dictionary<string, string> parameters) {
1314
}
1415

1516
public void LogResults(List<(Implementation, VerificationResult)> verificationResults) {
16-
foreach (var (implementation, result) in verificationResults) {
17+
var orderedResults = verificationResults.OrderBy(vr => vr.Item1.Name);
18+
foreach (var (implementation, result) in orderedResults) {
1719
tw.WriteLine("");
1820
tw.WriteLine($"Results for {implementation.Name}");
1921
tw.WriteLine($" Overall outcome: {result.Outcome}");
2022
tw.WriteLine($" Overall time: {result.End - result.Start}");
2123
tw.WriteLine($" Overall resource count: {result.ResourceCount}");
22-
foreach (var vcResult in result.VCResults) {
24+
foreach (var vcResult in result.VCResults.OrderBy(r => r.vcNum)) {
2325
tw.WriteLine("");
2426
tw.WriteLine($" Assertion batch {vcResult.vcNum}:");
2527
tw.WriteLine($" Outcome: {vcResult.outcome}");
@@ -36,4 +38,4 @@ public void LogResults(List<(Implementation, VerificationResult)> verificationRe
3638
}
3739
tw.Flush();
3840
}
39-
}
41+
}

0 commit comments

Comments
 (0)