Make trace output culture invariant

boogie-org · Aug 8, 2024 · 735fee4 · 735fee4
1 parent 2870fb0
commit 735fee4
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 10 deletions.
diff --git 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
@@ -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,