test: port the downstream DateTime round-trip suite onto the ticks encoding

[jsboige]

Stacked test PR from the downstream fork (MyIntelligenceAgency/Z3.Linq): the DateTime round-trip suite we wrote against the defect this PR fixes, ported onto this branch's harness — an independent double-check from the outside, with shapes chosen before we ever saw your fix.

What it adds

Four facts in solutions/Z3.Linq.Tests/DateTimeRoundTripTests.cs, our #14445 investigation reduced to tests:

Test	Shape
Solve_DateTimeBefore1601_RoundTrips	1500-01-01 round-trips as UTC (the write half of #83)
Solve_DateTime_RoundTripsAsUtcWithSameTicks	a 2026 instant keeps both its ticks and DateTimeKind.Utc — the two asserted separately, so a local-time read cannot pass as a UTC one on any runner
Solve_DateTimeListBefore1601_RoundTripsEveryElement	1582-10-15 inside a List<DateTime> — the collection arm (complements your DateTime[] test with the List environment)
Solve_DateTimeBeyondRange_ThrowsNamingTheSymbol	> max throws OverflowException naming the symbol

The environments are declared locally and name their symbol D, so the guard's message is pinned on a second name besides the X1 of SymbolTypeMarshallingTests — the same guarantee with a different label.

One adaptation

The beyond-range bound is captured into a local first (DateTime max = DateTime.MaxValue;), exactly as SymbolTypeMarshallingTests already does: a static field member in the tree is not partial-evaluated away on this branch, and translation refuses it (NotSupportedException). Worth knowing if anyone writes the bound inline in a notebook later.

Red on feature/xml-docs (this PR's base), same suite, same machine

échec Solve_DateTimeBefore1601_RoundTrips (132ms)
  System.ArgumentOutOfRangeException: Not a valid Win32 FileTime.
    sur System.DateTime.ToFileTimeUtc()          <- write path
échec Solve_DateTimeListBefore1601_RoundTripsEveryElement (121ms)
  System.ArgumentOutOfRangeException: Not a valid Win32 FileTime.
    sur System.DateTime.ToFileTimeUtc()          <- write path
échec Solve_DateTimeBeyondRange_ThrowsNamingTheSymbol (167ms)
      should throw System.OverflowException but threw
  System.ArgumentOutOfRangeException: Not a valid Win32 FileTime. (Parameter 'fileTime')
    sur System.DateTime.FromFileTimeUtc(Int64)   <- read path, blaming the caller
Résumé: total: 251, échec: 3, réussi: 248

The fourth test (RoundTripsAsUtcWithSameTicks) passes on the base as well — that is the #56 behaviour this PR deliberately preserves, and the port pins it so the fix cannot regress it in passing.

Green on this branch

Résumé: total: 258, échec: 0, réussi: 258

(254 from this PR's suite + the 4 ported; dotnet run on the MTP project, net10.0, win-x64.)

🤖 Generated with Claude Code