From ba8ded57a4d4059dbc591129d3a999136eea9e23 Mon Sep 17 00:00:00 2001 From: Howard van Rooijen Date: Tue, 1 Sep 2026 17:40:56 +0100 Subject: [PATCH 1/2] Render real constants invariantly ExpressionVisitor handed real constants to Z3 with the current culture, so a comma-decimal culture produced "1,5" and Z3's parser rejected it. Measured over the 606 specific cultures installed on this machine, 301 of them - about half - could not solve a theorem containing a real literal. The two culture tests move out of SymbolTypeMarshallingTests into a file of their own, joined by coverage for the negative-sign and non-comma-separator cases that a naive fix would miss. Fixes #52. Co-Authored-By: Claude Opus 5 (1M context) --- .../Z3.Linq.Tests/CultureInvarianceTests.cs | 260 ++++++++++++++++++ solutions/Z3.Linq.Tests/RewriterTests.cs | 4 +- .../SymbolTypeMarshallingTests.cs | 106 +------ .../UnsupportedExpressionTests.cs | 6 +- solutions/Z3.Linq/ExpressionVisitor.cs | 5 +- 5 files changed, 270 insertions(+), 111 deletions(-) create mode 100644 solutions/Z3.Linq.Tests/CultureInvarianceTests.cs diff --git a/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs b/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs new file mode 100644 index 0000000..b92aeef --- /dev/null +++ b/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs @@ -0,0 +1,260 @@ +namespace Z3.Linq.Tests; + +using System.Globalization; +using System.Runtime.ExceptionServices; +using System.Threading; + +/// +/// Pins that translating a C# constant into a Z3 term does not depend on the ambient culture. +/// +/// +/// +/// Z3's parser accepts only . as a decimal separator and only ASCII - as a sign, +/// so a number handed to it has to be rendered invariantly. Until #52 was fixed, +/// ExpressionVisitor rendered real constants with the current culture. Measured over the +/// 606 specific cultures installed on the development machine, 301 of them produced a literal +/// Z3 rejected with Z3Exception: parser error - about half, and every widely used +/// European language among them. None produced a wrong value, which is the one merciful thing +/// about it: the defect always announced itself. +/// +/// +/// Every test here runs its solve on a dedicated thread. CurrentCulture is per-thread, +/// these tests run in parallel at method level, and the runner hands out pooled threads - so +/// setting it on the test's own thread could leak into whatever runs next on that thread. A +/// thread created for the purpose cannot leak anywhere. +/// +/// +/// Each culture test starts by asserting that the culture really does render its probe value +/// differently from the invariant culture. Under globalization-invariant mode every culture +/// falls back to invariant data, and without that check these tests would pass while +/// exercising nothing. +/// +/// +/// The solve, the model and the read back all happen on the foreign-culture thread, so these +/// cover the whole round trip rather than the write side alone. +/// +/// +[TestClass] +public class CultureInvarianceTests +{ + /// + /// How long to wait for a solve running on a dedicated thread. Generous by design - it + /// exists to turn a hang into a failure, not to police how long a solve should take. + /// + private static readonly TimeSpan SolveTimeout = TimeSpan.FromSeconds(30); + + [TestMethod] + [DataRow("de-DE", DisplayName = "German - comma separator")] + [DataRow("fr-FR", DisplayName = "French - comma separator")] + [DataRow("ru-RU", DisplayName = "Russian - comma separator")] + [DataRow("tr-TR", DisplayName = "Turkish - comma separator")] + [DataRow("fa-IR", DisplayName = "Persian - U+066B decimal separator")] + public void Solve_DoubleConstantUnderANonInvariantCulture_RoundTripsTheValue(string culture) + { + // Arrange: the case in #52's title. fa-IR is here because its separator is not a comma + // either - the defect was never specific to one character. + RequireANonInvariantRendering(culture, 1.5); + + // Act + double? value = SolveOn(culture, () => + { + using var context = new Z3Context(); + return context.NewTheorem>() + .Where(t => t.X1 == 1.5) + .Solve()?.X1; + }); + + // Assert + value.ShouldBe(1.5); + } + + /// + /// A negative real constant survives a culture whose negative sign is not ASCII. + /// + /// + /// These cultures render -1.5 with U+2212 MINUS SIGN rather than ASCII -. A fix that + /// only swapped the decimal separator would still hand Z3 a sign it cannot parse, so this is + /// the case that rules out the obvious wrong fix. + /// + [TestMethod] + [DataRow("sv-SE", DisplayName = "Swedish")] + [DataRow("fi-FI", DisplayName = "Finnish")] + public void Solve_NegativeDoubleConstantUnderACultureWithANonAsciiSign_RoundTripsTheValue( + string culture) + { + // Arrange + CultureInfo.GetCultureInfo(culture).NumberFormat.NegativeSign.ShouldNotBe("-"); + RequireANonInvariantRendering(culture, -1.5); + + // Act + double? value = SolveOn(culture, () => + { + using var context = new Z3Context(); + return context.NewTheorem>() + .Where(t => t.X1 == -1.5) + .Solve()?.X1; + }); + + // Assert + value.ShouldBe(-1.5); + } + + [TestMethod] + [DataRow("de-DE", DisplayName = "German")] + [DataRow("sv-SE", DisplayName = "Swedish")] + public void Solve_DecimalConstantUnderANonInvariantCulture_RoundTripsTheValue(string culture) + { + // Arrange: decimal shares the real sort with double and the same arm of the constant + // switch, but it is a separate CLR formatter, so it gets its own case. + RequireANonInvariantRendering(culture, 1.5m); + + // Act + decimal? value = SolveOn(culture, () => + { + using var context = new Z3Context(); + return context.NewTheorem>() + .Where(t => t.X1 == 1.5m) + .Solve()?.X1; + }); + + // Assert + value.ShouldBe(1.5m); + } + + /// + /// A float constant gets past translation under a foreign culture and fails at the + /// read back instead - which is #54, not #52. + /// + /// + /// float takes the same arm of the constant switch as double and + /// decimal, so without this the fix would have a third of its call site untested. It + /// cannot be a round-trip test, because a float symbol cannot round-trip at all: the model + /// value is parsed into a double and reflection then refuses to write it to a float + /// property. Under the defect this threw Z3Exception during translation, so reaching + /// is itself the evidence that translation now succeeds. + /// + [TestMethod] + public void Solve_FloatConstantUnderANonInvariantCulture_FailsInMarshallingNotTranslation() + { + // Arrange + const string Culture = "de-DE"; + RequireANonInvariantRendering(Culture, 1.5f); + + // Act & Assert + Should.Throw(() => SolveOn(Culture, () => + { + using var context = new Z3Context(); + return context.NewTheorem>() + .Where(t => t.X1 == 1.5f) + .Solve()?.X1; + })); + } + + /// + /// A string constant is unaffected by the culture. + /// + /// + /// The line that fixes #52 sits two above a MkString(val.ToString()) that looks + /// identical. That one is safe - String.ToString() returns the instance - and this + /// test is here so the asymmetry is a recorded fact rather than an oversight waiting to be + /// tidied up. tr-TR because its casing rules are the usual way a string path turns out to + /// be culture-sensitive after all. + /// + [TestMethod] + public void Solve_StringConstantUnderANonInvariantCulture_RoundTripsTheValue() + { + // Arrange + const string Culture = "tr-TR"; + CultureInfo.GetCultureInfo(Culture).TextInfo.ToLower("I").ShouldNotBe("i"); + + // Act + string? value = SolveOn(Culture, () => + { + using var context = new Z3Context(); + return context.NewTheorem>() + .Where(t => t.X1 == "III") + .Solve()?.X1; + }); + + // Assert + value.ShouldBe("III"); + } + + [TestMethod] + public void Solve_DoubleConstantUnderTheInvariantCulture_RoundTripsTheValue() + { + // Arrange: the control. It uses the same dedicated-thread mechanism as the tests above, + // so they differ from it by culture and nothing else. This one passed on both sides of + // the fix; if it ever fails, the problem is the harness rather than the culture. + + // Act + double? value = SolveOn(string.Empty, () => + { + using var context = new Z3Context(); + return context.NewTheorem>() + .Where(t => t.X1 == 1.5) + .Solve()?.X1; + }); + + // Assert + value.ShouldBe(1.5); + } + + /// + /// Asserts that renders differently from + /// the invariant culture, so a test using it can detect the defect it exists for. + /// + private static void RequireANonInvariantRendering(string culture, IFormattable probe) + { + CultureInfo cultureInfo = CultureInfo.GetCultureInfo(culture); + + cultureInfo.NumberFormat.NumberDecimalSeparator.ShouldNotBe( + CultureInfo.InvariantCulture.NumberFormat.NumberDecimalSeparator, + $"{culture} formats numbers exactly as the invariant culture does on this machine, " + + "so this test cannot detect the defect it exists for - most likely the runtime is " + + "in globalization-invariant mode, where every culture falls back to invariant " + + "data"); + + probe.ToString(null, cultureInfo) + .ShouldNotBe(probe.ToString(null, CultureInfo.InvariantCulture)); + } + + /// + /// Runs on a thread pinned to , and returns + /// what it returned or rethrows what it threw. + /// + /// + /// The exception is captured and rethrown rather than left to escape: one escaping a bare + /// thread is unhandled, so it takes down the test host and the run reports "zero tests ran" + /// rather than one failure. + /// + private static T SolveOn(string culture, Func body) + { + T result = default!; + ExceptionDispatchInfo? failure = null; + + var thread = new Thread(() => + { + CultureInfo.CurrentCulture = CultureInfo.GetCultureInfo(culture); + + try + { + result = body(); + } + catch (Exception ex) + { + failure = ExceptionDispatchInfo.Capture(ex); + } + }); + + thread.Start(); + + // Bounded, so that a solver that never returns fails the test rather than hanging the + // whole run with no indication of which test stopped. The work itself takes single-digit + // milliseconds, so the limit is enormous slack rather than a tuned value. + thread.Join(SolveTimeout).ShouldBeTrue($"the solve on the {culture} thread did not finish"); + + failure?.Throw(); + return result; + } +} diff --git a/solutions/Z3.Linq.Tests/RewriterTests.cs b/solutions/Z3.Linq.Tests/RewriterTests.cs index f5bbf02..da28e82 100644 --- a/solutions/Z3.Linq.Tests/RewriterTests.cs +++ b/solutions/Z3.Linq.Tests/RewriterTests.cs @@ -117,7 +117,7 @@ public void Solve_PredicateRewriterThatReturnsItsInput_ThrowsTheProgressGuard() { // Arrange: the visitor re-visits whatever the rewriter returns, so a rewriter returning // its own input would recurse forever. That is detected by reference equality and - // rejected (ExpressionVisitor.cs:191) - a guard worth keeping, since the alternative is + // rejected (ExpressionVisitor.cs:192) - a guard worth keeping, since the alternative is // a hung build rather than a failed one. using var context = new Z3Context(); var theorem = context.NewTheorem>() @@ -131,7 +131,7 @@ public void Solve_PredicateRewriterThatReturnsItsInput_ThrowsTheProgressGuard() public void Solve_PredicateRewriterTypeNotImplementingTheInterface_ThrowsInvalidOperationException() { // Arrange: as with the global rewriter, the attribute cannot enforce this at compile - // time (ExpressionVisitor.cs:179). + // time (ExpressionVisitor.cs:180). using var context = new Z3Context(); var theorem = context.NewTheorem>() .Where(t => WrongRewriterType(t.X1, t.X2)); diff --git a/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs b/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs index 600a2cb..aa9418f 100644 --- a/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs +++ b/solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs @@ -1,8 +1,5 @@ namespace Z3.Linq.Tests; -using System.Globalization; -using System.Threading; - /// /// Round-trips a value of each scalar symbol type through : /// C# constant -> Z3 term -> model -> CLR property. @@ -23,12 +20,6 @@ namespace Z3.Linq.Tests; [TestClass] public class SymbolTypeMarshallingTests { - /// - /// How long to wait for a solve running on a dedicated thread. Generous by design - it - /// exists to turn a hang into a failure, not to police how long a solve should take. - /// - private static readonly TimeSpan SolveTimeout = TimeSpan.FromSeconds(30); - [TestMethod] [DataRow(0, DisplayName = "Zero")] [DataRow(42, DisplayName = "Positive")] @@ -173,7 +164,7 @@ public void Solve_DoubleSymbolWithInequality_SatisfiesTheConstraint() /// /// A short symbol is created with MkIntConst, but C# widens short to int for the comparison /// and ExpressionVisitor.VisitUnary reads that Convert node as a real-to-int conversion, - /// casting the IntExpr to RealExpr (ExpressionVisitor.cs:131). A second defect waits behind + /// casting the IntExpr to RealExpr (ExpressionVisitor.cs:132). A second defect waits behind /// it: TypeCode.Int16 marshals to an int, which a short property rejects. /// This test pins current behaviour and must be updated when the defect is fixed. /// @@ -265,101 +256,6 @@ public void Solve_MixedTypeSymbols_MarshalsEveryPropertyIndependently() result.X2.ShouldBe("five"); } - /// - /// KNOWN DEFECT (#52): a real-valued constant is written to Z3 using the current culture. - /// - /// - /// - /// ExpressionVisitor.cs:304 calls MkReal(val.ToString()) with no format provider, so under a - /// comma-decimal culture the literal 1.5 is handed to Z3 as "1,5" and its parser rejects it. - /// Every other numeric conversion in the visitor passes InvariantCulture, and so does every - /// read back on the marshalling side, which is what makes this one look like an oversight - /// rather than a decision. - /// - /// - /// The work runs on a dedicated thread rather than by setting the culture on the test's own - /// thread. CurrentCulture is per-thread, these tests run in parallel at method level, and - /// the runner hands out pooled threads - so mutating it here could leak into whatever runs - /// next on the same thread. A thread created for the purpose cannot leak anywhere. - /// - /// This test pins current behaviour and must be updated when the defect is fixed. - /// - [TestMethod] - public void Solve_DoubleSymbolUnderCommaDecimalCulture_ThrowsZ3ParserError() - { - // Arrange - Exception? captured = null; - - var thread = new Thread(() => - { - CultureInfo.CurrentCulture = CultureInfo.GetCultureInfo("de-DE"); - - try - { - using var context = new Z3Context(); - _ = context.NewTheorem>() - .Where(t => t.X1 == 1.5) - .Solve(); - } - catch (Exception ex) - { - captured = ex; - } - }); - - // Act - thread.Start(); - - // Bounded, so that a solver that never returns fails this test rather than hanging the - // whole run with no indication of which test stopped. The work itself takes single-digit - // milliseconds, so the limit is enormous slack rather than a tuned value. - thread.Join(SolveTimeout).ShouldBeTrue("the solve on the de-DE thread did not finish"); - - // Assert - captured.ShouldBeOfType(); - } - - [TestMethod] - public void Solve_DoubleSymbolUnderInvariantCulture_RoundTripsTheValue() - { - // Arrange: the counterpart to the pin above, on the same dedicated-thread mechanism, so - // that the two differ only by culture. This is what the defect above should look like - // once it is fixed. - double? value = null; - Exception? captured = null; - - var thread = new Thread(() => - { - CultureInfo.CurrentCulture = CultureInfo.InvariantCulture; - - try - { - using var context = new Z3Context(); - var result = context.NewTheorem>() - .Where(t => t.X1 == 1.5) - .Solve(); - - value = result?.X1; - } - catch (Exception ex) - { - // Captured rather than left to escape: an exception on a bare thread is - // unhandled, so it takes down the test host and the run reports "zero tests - // ran" rather than one failed test. The pin above already does this; this - // counterpart did not, because it was not expected to throw. - captured = ex; - } - }); - - // Act - thread.Start(); - thread.Join(SolveTimeout).ShouldBeTrue("the solve on the invariant-culture thread did not finish"); - - // Assert - captured.ShouldBeNull(); - value.ShouldBe(1.5); - } - /// /// An unconstrained long symbol is populated rather than throwing. /// diff --git a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs index 1fb7f49..2a980ed 100644 --- a/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs +++ b/solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs @@ -50,7 +50,7 @@ public void Solve_CallToAnUnrecognisedMethod_ThrowsNotSupportedException() // Arrange: only Z3Methods.Distinct, indexed property getters and methods carrying a // predicate rewriter attribute are understood. An ordinary method that depends on a // theorem symbol cannot be evaluated away, so it reaches the visitor and is rejected - // (ExpressionVisitor.cs:277). + // (ExpressionVisitor.cs:278). using var context = new Z3Context(); var theorem = context.NewTheorem>() .Where(t => Increment(t.X1) == 2); @@ -64,7 +64,7 @@ public void Solve_UnsupportedCast_ThrowsNotImplementedException() { // Arrange: the Convert case handles conversions to double, int and char only. Widening // an int symbol to long is unremarkable C# but has no case, so it falls through to the - // catch-all (ExpressionVisitor.cs:140). Note this one is NotImplementedException rather + // catch-all (ExpressionVisitor.cs:141). Note this one is NotImplementedException rather // than NotSupportedException - the throw sites are not consistent about which they use. using var context = new Z3Context(); var theorem = context.NewTheorem>() @@ -119,7 +119,7 @@ public void Solve_NullableProperty_ThrowsArgumentException() /// /// An enum's TypeCode is that of its underlying type, so the symbol is created as an /// integer - and then C# emits a Convert to int for the comparison, which - /// ExpressionVisitor.cs:131 reads as a real-to-int conversion and casts to RealExpr. Same + /// ExpressionVisitor.cs:132 reads as a real-to-int conversion and casts to RealExpr. Same /// root cause as short, so the same fix covers both. /// This test pins current behaviour and must be updated when the defect is fixed. /// diff --git a/solutions/Z3.Linq/ExpressionVisitor.cs b/solutions/Z3.Linq/ExpressionVisitor.cs index 46509b2..bc9d6d5 100644 --- a/solutions/Z3.Linq/ExpressionVisitor.cs +++ b/solutions/Z3.Linq/ExpressionVisitor.cs @@ -1,6 +1,7 @@ namespace Z3.Linq; using System.Collections; +using System.Globalization; using System.Linq.Expressions; using System.Reflection; @@ -301,7 +302,9 @@ private static Expr VisitConstantValue(Context context, object val) case TypeCode.Single: case TypeCode.Double: case TypeCode.Decimal: - return context.MkReal(val.ToString()); + // Invariant, not current: Z3's parser accepts only '.' as the decimal separator, + // and about half of all cultures render 1.5 as something else. See #52. + return context.MkReal(((IFormattable)val).ToString(null, CultureInfo.InvariantCulture)); case TypeCode.DateTime: return context.MkInt(((DateTime)val).ToFileTimeUtc()); case TypeCode.String: From d25a1e53109b3fc5582679f43557ebc8279ce9d1 Mon Sep 17 00:00:00 2001 From: Howard van Rooijen Date: Tue, 1 Sep 2026 17:53:49 +0100 Subject: [PATCH 2/2] Let the culture harness time out cleanly The solve threads were foreground, so one that outlived its bounded Join would hold the test host open indefinitely - measured: a process whose Main has returned does not exit at all while a foreground thread is still running. That turned the timeout from a clean failure into a stalled run. SolveOn now takes the resolved CultureInfo rather than a name, so the control test names the invariant culture instead of passing an empty string, and the timeout message has something to say for it. Co-Authored-By: Claude Opus 5 (1M context) --- .../Z3.Linq.Tests/CultureInvarianceTests.cs | 46 ++++++++++++------- 1 file changed, 29 insertions(+), 17 deletions(-) diff --git a/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs b/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs index b92aeef..560fe85 100644 --- a/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs +++ b/solutions/Z3.Linq.Tests/CultureInvarianceTests.cs @@ -53,10 +53,10 @@ public void Solve_DoubleConstantUnderANonInvariantCulture_RoundTripsTheValue(str { // Arrange: the case in #52's title. fa-IR is here because its separator is not a comma // either - the defect was never specific to one character. - RequireANonInvariantRendering(culture, 1.5); + CultureInfo cultureInfo = RequireANonInvariantRendering(culture, 1.5); // Act - double? value = SolveOn(culture, () => + double? value = SolveOn(cultureInfo, () => { using var context = new Z3Context(); return context.NewTheorem>() @@ -83,11 +83,11 @@ public void Solve_NegativeDoubleConstantUnderACultureWithANonAsciiSign_RoundTrip string culture) { // Arrange - CultureInfo.GetCultureInfo(culture).NumberFormat.NegativeSign.ShouldNotBe("-"); - RequireANonInvariantRendering(culture, -1.5); + CultureInfo cultureInfo = RequireANonInvariantRendering(culture, -1.5); + cultureInfo.NumberFormat.NegativeSign.ShouldNotBe("-"); // Act - double? value = SolveOn(culture, () => + double? value = SolveOn(cultureInfo, () => { using var context = new Z3Context(); return context.NewTheorem>() @@ -106,10 +106,10 @@ public void Solve_DecimalConstantUnderANonInvariantCulture_RoundTripsTheValue(st { // Arrange: decimal shares the real sort with double and the same arm of the constant // switch, but it is a separate CLR formatter, so it gets its own case. - RequireANonInvariantRendering(culture, 1.5m); + CultureInfo cultureInfo = RequireANonInvariantRendering(culture, 1.5m); // Act - decimal? value = SolveOn(culture, () => + decimal? value = SolveOn(cultureInfo, () => { using var context = new Z3Context(); return context.NewTheorem>() @@ -138,10 +138,10 @@ public void Solve_FloatConstantUnderANonInvariantCulture_FailsInMarshallingNotTr { // Arrange const string Culture = "de-DE"; - RequireANonInvariantRendering(Culture, 1.5f); + CultureInfo cultureInfo = RequireANonInvariantRendering(Culture, 1.5f); // Act & Assert - Should.Throw(() => SolveOn(Culture, () => + Should.Throw(() => SolveOn(cultureInfo, () => { using var context = new Z3Context(); return context.NewTheorem>() @@ -165,10 +165,11 @@ public void Solve_StringConstantUnderANonInvariantCulture_RoundTripsTheValue() { // Arrange const string Culture = "tr-TR"; - CultureInfo.GetCultureInfo(Culture).TextInfo.ToLower("I").ShouldNotBe("i"); + CultureInfo cultureInfo = CultureInfo.GetCultureInfo(Culture); + cultureInfo.TextInfo.ToLower("I").ShouldNotBe("i"); // Act - string? value = SolveOn(Culture, () => + string? value = SolveOn(cultureInfo, () => { using var context = new Z3Context(); return context.NewTheorem>() @@ -188,7 +189,7 @@ public void Solve_DoubleConstantUnderTheInvariantCulture_RoundTripsTheValue() // the fix; if it ever fails, the problem is the harness rather than the culture. // Act - double? value = SolveOn(string.Empty, () => + double? value = SolveOn(CultureInfo.InvariantCulture, () => { using var context = new Z3Context(); return context.NewTheorem>() @@ -204,7 +205,8 @@ public void Solve_DoubleConstantUnderTheInvariantCulture_RoundTripsTheValue() /// Asserts that renders differently from /// the invariant culture, so a test using it can detect the defect it exists for. /// - private static void RequireANonInvariantRendering(string culture, IFormattable probe) + /// The resolved culture, so the caller resolves it once. + private static CultureInfo RequireANonInvariantRendering(string culture, IFormattable probe) { CultureInfo cultureInfo = CultureInfo.GetCultureInfo(culture); @@ -217,6 +219,8 @@ private static void RequireANonInvariantRendering(string culture, IFormattable p probe.ToString(null, cultureInfo) .ShouldNotBe(probe.ToString(null, CultureInfo.InvariantCulture)); + + return cultureInfo; } /// @@ -228,14 +232,14 @@ private static void RequireANonInvariantRendering(string culture, IFormattable p /// thread is unhandled, so it takes down the test host and the run reports "zero tests ran" /// rather than one failure. /// - private static T SolveOn(string culture, Func body) + private static T SolveOn(CultureInfo culture, Func body) { T result = default!; ExceptionDispatchInfo? failure = null; var thread = new Thread(() => { - CultureInfo.CurrentCulture = CultureInfo.GetCultureInfo(culture); + CultureInfo.CurrentCulture = culture; try { @@ -245,14 +249,22 @@ private static T SolveOn(string culture, Func body) { failure = ExceptionDispatchInfo.Capture(ex); } - }); + }) + { + // Foreground is the default, and a foreground thread that outlives the wait below + // holds the whole test host open - measured: a process whose Main has returned does + // not exit at all while one is still running. That turns the timeout from a clean + // failure into a stalled run, which is the opposite of what it is here for. + IsBackground = true, + }; thread.Start(); // Bounded, so that a solver that never returns fails the test rather than hanging the // whole run with no indication of which test stopped. The work itself takes single-digit // milliseconds, so the limit is enormous slack rather than a tuned value. - thread.Join(SolveTimeout).ShouldBeTrue($"the solve on the {culture} thread did not finish"); + string name = culture.Name.Length == 0 ? "invariant" : culture.Name; + thread.Join(SolveTimeout).ShouldBeTrue($"the solve on the {name} thread did not finish"); failure?.Throw(); return result;