From 735fee450f154912d5f04069a401c9dd603805a5 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 8 Aug 2024 15:53:48 +0200
Subject: [PATCH] Make trace output culture invariant

---
 Source/Provers/SMTLib/TypeDeclCollector.cs  | 16 ++++++++--------
 Source/VCGeneration/SplitAndVerifyWorker.cs |  6 ++++--
 2 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 6f034db03..dac076b12 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -15,7 +15,7 @@ public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool>
     private UniqueNamer Namer;
 
     private HashSet<Function /*!*/> /*!*/
-      RegisteredRelations = new HashSet<Function>();
+      RegisteredRelations = new();
 
     [ContractInvariantMethod]
     void ObjectInvariant()
@@ -43,8 +43,8 @@ protected override bool StandardResult(VCExpr node, bool arg)
       return true;
     }
 
-    private readonly List<string /*!>!*/> AllDecls = new List<string /*!*/>();
-    private readonly List<string /*!>!*/> IncDecls = new List<string /*!*/>();
+    private readonly List<string /*!>!*/> AllDecls = new();
+    private readonly List<string /*!>!*/> IncDecls = new();
 
     // In order to support push/pop interface of the theorem prover, the "known" declarations
     // must be kept in a stack
@@ -75,12 +75,12 @@ private HashSet<string /*!*/> /*!*/ KnownSelectFunctions
     }
 
     // ------
-    private readonly Stack<HashSet<Function /*!*/> /*!*/> _KnownFunctions = new Stack<HashSet<Function /*!*/>>();
-    private readonly Stack<HashSet<VCExprVar /*!*/> /*!*/> _KnownVariables = new Stack<HashSet<VCExprVar /*!*/>>();
+    private readonly Stack<HashSet<Function /*!*/> /*!*/> _KnownFunctions = new();
+    private readonly Stack<HashSet<VCExprVar /*!*/> /*!*/> _KnownVariables = new();
 
-    private readonly Stack<HashSet<Type /*!*/> /*!*/> _KnownTypes = new Stack<HashSet<Type>>();
-    private readonly Stack<HashSet<string /*!*/> /*!*/> _KnownStoreFunctions = new Stack<HashSet<string>>();
-    private readonly Stack<HashSet<string /*!*/> /*!*/> _KnownSelectFunctions = new Stack<HashSet<string>>();
+    private readonly Stack<HashSet<Type /*!*/> /*!*/> _KnownTypes = new();
+    private readonly Stack<HashSet<string /*!*/> /*!*/> _KnownStoreFunctions = new();
+    private readonly Stack<HashSet<string /*!*/> /*!*/> _KnownSelectFunctions = new();
 
     private void InitializeKnownDecls()
     {
diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs
index c5a0333a5..2fbe080a9 100644
--- a/Source/VCGeneration/SplitAndVerifyWorker.cs
+++ b/Source/VCGeneration/SplitAndVerifyWorker.cs
@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Globalization;
 using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
@@ -139,8 +140,9 @@ private async Task StartCheck(int iteration, Split split, Checker checker, Cance
       {
         var splitNum = split.SplitIndex + 1;
         var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}";
-        run.OutputWriter.WriteLine("    checking split {1}/{2}, {3:0.00}%, {0} ...",
-          split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost));
+        await run.OutputWriter.WriteLineAsync(string.Format(CultureInfo.InvariantCulture, 
+          "    checking split {1}/{2}, {3:0.00}%, {0} ...",
+          split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost)));
       }
 
       callback.OnProgress?.Invoke("VCprove", split.SplitIndex, total,