Render real constants invariantly

[HowardvanRooijen]

Fixes #52.

The defect

ExpressionVisitor rendered every real constant with the ambient culture:

return context.MkReal(val.ToString());

Z3's parser accepts only . as a decimal separator and only ASCII - as a sign, so under a
comma-decimal culture the literal 1.5 arrived as "1,5":

CultureInfo.CurrentCulture = CultureInfo.GetCultureInfo("de-DE");
using var ctx = new Z3Context();
ctx.NewTheorem<Symbols<double, int>>().Where(t => t.X1 == 1.5).Solve();
// Microsoft.Z3.Z3Exception: parser error

It is much wider than the comma. Sweeping all 606 specific cultures installed on this
machine, solving X1 == 1.5:

	Before	After
Round-tripped correctly	305	606
Rejected with parser error	301	0
Silently wrong value	0	0

About half of all cultures, including every widely used European language. The one merciful
thing is the last row: no culture produced a wrong answer, so the defect always announced
itself rather than quietly corrupting a model.

The separator is not the only character involved:

Culture	(1.5).ToString()	(-1.5).ToString()
en-GB, hi-IN	1.5	-1.5
de-DE, fr-FR, ru-RU, tr-TR	1,5	-1,5
sv-SE, fi-FI, nb-NO	1,5	−1,5 - U+2212 MINUS SIGN, not ASCII
fa-IR, ar-EG	1٫5 - U+066B	؜-1٫5

The change

One line, plus the using it needs:

case TypeCode.Single:
case TypeCode.Double:
case TypeCode.Decimal:
    return context.MkReal(((IFormattable)val).ToString(null, CultureInfo.InvariantCulture));

val is an object, and object.ToString() has no format-provider overload. The
IFormattable cast is safe here and preserves the existing formatting exactly: the switch is on
Type.GetTypeCode(val.GetType()), so the runtime type is float, double or decimal, all of
which implement it, and ToString(null, provider) is what each type's own
ToString(IFormatProvider) calls. Only the provider changes.

The using System.Globalization; shifts every line in the file by one, so the six
ExpressionVisitor.cs:NNN citations in the test suite are updated in the same commit. Each was
checked against its target line before and after.

The rest of the file was already right. Convert.ToInt64 for the integer arm performs no
formatting, and the MkString(val.ToString()) two lines below is String.ToString(), which
returns the instance. That asymmetry now has a test rather than being left to look like an
oversight.

Tests

145 → 155. The two culture tests move out of SymbolTypeMarshallingTests into
CultureInvarianceTests: the subject is the constant visitor rather than symbol marshalling,
the dedicated-thread harness is now shared by six tests, and the extraction takes
System.Threading and SolveTimeout out of a file that no longer needs them.

The solve threads are background threads. Measured: a process whose Main has returned does not
exit at all while a foreground thread is still running, so a solve that outlived the bounded
Join would have held the whole test host open - turning the timeout from a clean failure into
a stalled run. The two tests this replaces had the same flaw; it is worth fixing once now that
six tests share the harness.

Test	Cultures	Why
Solve_DoubleConstantUnderANonInvariantCulture_RoundTripsTheValue	de-DE, fr-FR, ru-RU, tr-TR, fa-IR	the case in the issue title, plus a non-comma separator
Solve_NegativeDoubleConstantUnderACultureWithANonAsciiSign_RoundTripsTheValue	sv-SE, fi-FI	U+2212 minus - the case a separator-only fix would miss
Solve_DecimalConstantUnderANonInvariantCulture_RoundTripsTheValue	de-DE, sv-SE	separate CLR formatter, same switch arm
Solve_FloatConstantUnderANonInvariantCulture_FailsInMarshallingNotTranslation	de-DE	the third type on that arm - see below
Solve_StringConstantUnderANonInvariantCulture_RoundTripsTheValue	tr-TR	pins the neighbouring line as deliberately unchanged
Solve_DoubleConstantUnderTheInvariantCulture_RoundTripsTheValue	invariant	the control, on the same harness

Each culture test first asserts that the culture really does render its probe differently from
the invariant one. Under globalization-invariant mode every culture falls back to invariant data
and these tests would otherwise pass while exercising nothing - a green that means the opposite
of what it looks like.

The float case cannot be a round-trip test, because a float symbol cannot round-trip at all
(#54). It asserts ArgumentException instead: under the defect it threw Z3Exception during
translation, so reaching the marshalling failure is the evidence that the TypeCode.Single
arm is now correct. Without it, a third of the fixed call site would be untested.

The issue says the defect was "deliberately not covered by a test", on the grounds that
CurrentCulture is per-thread and the suite runs in parallel at method level. That reasoning
holds for setting the culture on the test's own thread, but the pin added later already solved
it by running the solve on a thread created for the purpose, which cannot leak anywhere. This
PR generalises that harness rather than working around the constraint again.

Mutation results

Mutation	Failures	Which
Revert to val.ToString()	10	all five double rows, both negative rows, both decimal rows, and the float test. The string test and the invariant control stay green.
val.ToString().Replace(',', '.') - the naive fix	3	fa-IR (U+066B separator), sv-SE and fi-FI (U+2212 sign). Everything a comma-only fix handles passes, which is the point of those three rows.
Hard-code MkReal("0")	17	all 11 culture cases that assert a value, plus 6 pre-existing tests. Confirms the new tests assert the value rather than the absence of an exception.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 155/155 locally, 1.7s
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage unchanged at 75.8% line / 69.3% branch: the new tests exercise lines the suite
  already reached, under a different culture

Found along the way

#76 - comparing a real symbol against a float variable throws InvalidCastException.
C# inserts a Convert(Single -> Double), and VisitUnary picks the conversion from the target
type alone, so it treats an already-real operand as an integer. Same root cause as #63, one arm
along. Raised, not fixed.

Considered and rejected: running the whole suite under a foreign culture via an
AssemblyInitialize hook. It would have caught this class of defect everywhere rather than at
one call site, but it changes the environment of all 155 tests to catch a defect at one, and
makes every future failure culture-dependent to reproduce.

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org, so this reaches
main but not consumers. Nothing about the hold changes.

[Copilot]

Pull request overview

This PR fixes culture-sensitive rendering of real (float/double/decimal) constants when translating C# expressions to Z3, ensuring literals are formatted using invariant culture so Z3’s parser consistently accepts them across locales (fixing #52). It also restructures and expands test coverage to pin culture-invariant behavior (including non-ASCII minus sign and non-comma decimal separator cases).

Changes:

• Format real-valued constants using CultureInfo.InvariantCulture when calling Context.MkReal(...).
• Move prior culture-specific tests out of SymbolTypeMarshallingTests and add a dedicated CultureInvarianceTests suite.
• Update test comments that reference ExpressionVisitor line numbers.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
solutions/Z3.Linq/ExpressionVisitor.cs	Uses invariant formatting for real constants before handing literals to Z3.
solutions/Z3.Linq.Tests/UnsupportedExpressionTests.cs	Updates line-number references in comments after code movement.
solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs	Removes culture-related tests and shared timeout from this suite.
solutions/Z3.Linq.Tests/RewriterTests.cs	Updates line-number references in comments after code movement.
solutions/Z3.Linq.Tests/CultureInvarianceTests.cs	Adds dedicated, threaded culture-invariance tests covering decimals, signs, separators, and control cases.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[HowardvanRooijen]

Both taken, in d25a1e5 - the first as a correctness fix, the second as readability.

The background thread is a real finding. Measured with a process whose Main returns
after a bounded Join times out on a still-running thread:

IsBackground	Process exited within 8s
false (the default, what this had)	no - still alive at 8s, killed
true	yes, after 246ms

So the timeout was producing a stalled run rather than a clean failure, exactly as you describe.
The harness inherited that from the two tests it replaces, but it now backs six of them, so it
is worth getting right. Fixed, with the measurement recorded in a comment next to it.

GetCultureInfo("") was not relying on anything undocumented, though. The empty string is
the invariant culture's actual Name, and it resolves to it - measured: Equals true, LCID 127
(same as CultureInfo.InvariantCulture), decimal separator .. Not reference-equal, which does
not matter here.

What was genuinely poor was the call site: SolveOn(string.Empty, ...) in the control test
reads like an oversight, and the timeout message came out as "the solve on the thread did not
finish" with a hole in it. So rather than special-case the empty name - a branch guarding
against something that already works - SolveOn now takes the resolved CultureInfo. The
control test says CultureInfo.InvariantCulture, each culture test resolves its culture once
instead of twice, and the message falls back to "invariant" for the nameless one.

Verified: 155/155, and reverting the fix still fails exactly the same 10 tests as before the
change, so the harness rework did not blunt anything.

[github-actions]

Test Results

  1 files  ± 0    1 suites  ±0   4s ⏱️ ±0s
151 tests + 9  151 ✅ + 9  0 💤 ±0  0 ❌ ±0 
155 runs  +10  155 ✅ +10  0 💤 ±0  0 ❌ ±0 

Results for commit d25a1e5. ± Comparison against base commit 445aad0.

♻️ This comment has been updated with latest results.