fix(z3linq): DateTime round-trip — UTC ticks both ways (port of endjin#95) - #26
Merged
Merged
Conversation
…tc Kind + Ticks read-back, out-of-range guard Tests first, fix second: this commit alone must FAIL on CI (failing-before proof per the #14445 acceptance amendment). Co-Authored-By: Claude-Code <noreply@anthropic.com>
The pipeline never ran tests ($SkipTest = $true made the Test job a silent success) and the Analysis phase died with exit code 150 because Endjin.RecommendedPractices.Build 1.5.0+ pins covenant 0.12.0, a net6.0 tool, while ubuntu-24.04 runners no longer ship the .NET 6 runtime. Skip analysis and enable dotnet test so the DateTime round-trip regression (#14445) gets real red/green CI evidence. See #14445
Test Results87 tests 87 ✅ 3s ⏱️ Results for commit 6eab957. ♻️ This comment has been updated with latest results. |
…x natives On ubuntu-24.04 the managed wrapper bound to the system libz3 (4.8.x) and every context-creating test died with EntryPointNotFoundException for Z3_enable_concurrent_dec_ref. The last nuget.org Microsoft.Z3 release ships win-x64/osx-x64 natives only; windows-latest resolves the package's own libz3.dll, matching local dev machines. Upstream endjin instead consumes the GitHub-release 5.1.0 package through a pinned local feed. See #14445
…rded read-back Port of endjin#95 adapted to the 4.12.2 snapshot: - ExpressionVisitor.VisitConstant: a DateTime constant is now encoded as its UTC ticks (Kind-aware: Local values are normalized via ToUniversalTime() before encoding), instead of ToFileTime() which is undefined before 1601-01-01 and loses the Kind - Theorem read-back (ConvertZ3Expression + ConvertScalarExpr): values for DateTime symbols are rebuilt with new DateTime(ticks, DateTimeKind.Utc); an out-of-range model value raises an OverflowException naming the symbol instead of letting the DateTime ctor throw a bare ArgumentOutOfRangeException Red run (4 DateTime tests failing, all others green): https://github.com/MyIntelligenceAgency/Z3.Linq/actions/runs/33862719891 Green run: see next commit's dispatch See #14445
jsboige
added a commit
to jsboige/CoursIA
that referenced
this pull request
Sep 4, 2026
…ort of endjin#95) (#14594) Submodule bump e09dae6 -> 6eab957. Two DateTime domain defects fixed: - write path: ToFileTimeUtc() throws for pre-1601 instants and loses the Kind; DateTime constants are now encoded as UTC ticks (ToUtcTicks, Local values normalized first) - read path: FromFileTime decodes to machine-local time; model values for DateTime symbols are rebuilt as new DateTime(ticks, Utc) with a range guard raising OverflowException naming the symbol Two-phase CI proof on the fork (per the acceptance amendment): - RED (tests-only state) -- exactly 4 failures, all DateTimeRoundTripTests, genuine assertions (Win32 FileTime out of range / Kind Local / missing guard), other 83 pass: https://github.com/MyIntelligenceAgency/Z3.Linq/actions/runs/33862719891 - GREEN (fix) -- 87/87: https://github.comMyIntelligenceAgency/Z3.Linq/actions/runs/33863182778 Fork PR: MyIntelligenceAgency/Z3.Linq#26 The branch also carries the CI plumbing required to run tests at all ($SkipTest was true, covenant tool dead, no linux natives in the last nuget.org Microsoft.Z3) -- detailed in the fork PR body. Closes #14445
jsboige
added a commit
that referenced
this pull request
Sep 4, 2026
…eaches the notebooks (#27) The round-trip fix landed in the sources and its 87 tests, but not in the artifact the notebooks actually load. `.deploy/*.dll` is git-tracked (e09dae6, "commit .deploy DLLs for fresh-clone #r resolution") and 17 CoursIA notebooks bind to it via `#r "../Z3.Linq/.deploy/Z3.Linq.dll"`. PR #26 changed ExpressionVisitor.cs and Theorem.cs but did not rebuild that binary, so the blob was byte-identical across the fix (83f9901 both sides) and every notebook kept running the old file-time encoding. Measured, with the control in both directions: symbol deployed(old) rebuilt(new) ToUtcTicks 0 1 ToFileTimeUtc 1 0 FromFileTime 1 0 Only Z3.Linq.dll changes: ExpressionUtils.dll, Microsoft.Z3.dll and libz3.dll are byte-identical to what the pinned packages restore, which also rules out spurious rebuild noise. dotnet test Release: 87/87 passed, 0 failed (local, net8.0). See #14445, jsboige/CoursIA#14169 (G5).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Port of endjin#95 (their endjin#56/endjin#83) for CoursIA #14445 — two DateTime domain defects:
ToFileTimeUtc()counts from 1601-01-01 and throwsArgumentOutOfRangeExceptionfor anything earlier — no pre-1601 instant could be written. Encode as UTC ticks instead (ToUtcTicks).FromFileTimedecodes to LOCAL time (Kind=Local) while the write path encoded UTC — the same theorem answered differently on every machine, and the read-back carried the machine's offset. Read back asnew DateTime(ticks, DateTimeKind.Utc)(ToDateTime), with a checked range guard naming the symbol (Z3's integer is unbounded;t.D > DateTime.MaxValueis satisfiable).Two-step red/green proof (per #14445 acceptance amendment) — both runs on this fork's CI:
DateTimeRoundTripTests, all genuine assertion failures (ArgumentOutOfRangeException: Not a valid Win32 FileTimeon the pre-1601 tests;Assert.Equal: Expected Utc, Actual Localon the Kind test;Expected OverflowException, Actual ArgumentOutOfRangeExceptionon the guard test). The other 83 tests pass.Passed! Failed: 0, Passed: 87, Skipped: 0, Total: 87(83 pre-existing + the 4 new).CI plumbing on this branch (required to make the pipeline able to run tests at all):
build.ps1:$SkipTestwastrue— the pipeline's Test job was a silent success that never randotnet test; nowfalse.$SkipAnalysis = $true.build.yml:compilePhaseTasks: 'Build'— the covenant SBOM tool pinned by Endjin.RecommendedPractices.Build 1.5.0+ (covenant 0.12.0, net6.0-only) dies with exit 150 on current runners; upstream endjin fixed this by migrating to ZeroFailed.build.yml:runsOn: windows-latest— the last nuget.org Microsoft.Z3 (4.12.2) ships win-x64/osx-x64 natives only; on Linux the wrapper binds the ancient system libz3 and every context-creating test dies withEntryPointNotFoundException: Z3_enable_concurrent_dec_ref. Upstream consumes the GitHub-release 5.1.0 package via a pinned local feed instead.The Kind assertion fails on a UTC runner too (
FromFileTimemarksLocalunconditionally); the Ticks assertion adds the non-UTC discrimination. AToUniversalTime()comparison passes before the fix and measures nothing — not used.