[jsboige]

Why

CoursIA PR jsboige/CoursIA#22570 bumps its submodule to this fork. Its coordinator review was blocked on one compatibility point: the notebooks load .deploy/Z3.Linq.dll directly (#r "../Z3.Linq/.deploy/Z3.Linq.dll") on a .NET 8/9 runtime, while the published artifact only targeted net10.0 after the port.

This restores the pre-port compatibility at the fork level, without changing the solver source or the net10 build.

Change

• Z3.Linq.csproj clears the singular TargetFramework inherited from solutions/Directory.Build.props and declares TargetFrameworks=net8.0;net10.0. Without the clear, the SDK only builds the inherited net10.0 outer build.
• LangVersion is pinned to 14.0. The SDK otherwise infers C# 12 for the net8 target and rejects the C# 14 field keyword used by Z3Context, so the two targets would not compile the same source. The keyword is compiler-level and emits a normal backing field; it does not require a .NET 10 runtime.
• .deploy/Z3.Linq.dll is rebuilt from net8.0. The other three deployed files are byte-identical to the previous deploy set:
  • ExpressionUtils.dll f3847aee... (94208 bytes)
  • Microsoft.Z3.dll 47285bcd... (265728 bytes)
  • libz3.dll f4ea9e79... (18313728 bytes)

No solver source file changes.

Validation

Check	Result
dotnet build -c Release	both net8.0 and net10.0 produced, 0 warnings, 0 errors
net8 artifact marker	.NETCoreApp,Version=v8.0 (54a2d76efba3a776f1457b4a102d3d44243fe97db2664db6699e1e27c31a3c29)
net10 artifact marker	.NETCoreApp,Version=v10.0 (d1bc715f58641bfaafdedeb4cc1bc3e6558f2590c03bfffef89e6b3cf5d6f696)
dotnet publish -f net8.0	succeeded, published set contains all four consumers
net10 test suite	437/437 passed, 0 failed, 0 skipped, 5.145 s
net8 test suite	437/437 passed, 0 failed, 0 skipped, 4.697 s (same test sources compiled against the published net8 assembly)
net8 real-runtime smoke test	SOLVED (True, False), FRAMEWORK .NETCoreApp,Version=v8.0

The net8 suite is the repository's complete Z3.Linq.Tests source set plus its Z3.Linq.Examples source, compiled in a scratch harness targeting net8.0 and referencing the published net8 assembly. The repository test project itself stays on its inherited net10 target.

The smoke test is a net8.0 console app that loads the published net8 assembly and its unchanged dependencies, sets Timeout and ResourceLimit (the C# 14 field properties), and solves an XOR theorem through Solve().

Follow-up

Once this fork PR is merged, the CoursIA submodule pointer in #22570 can be rebumped to the merge commit and the parent review can be re-run against a chain that keeps both the net10 build and the net8 notebook artifact.

🤖 Generated with Claude Code

[github-actions]

Code Coverage Summary Report - Linux (No TFM)

Summary

Generated on:	10/26/2026 - 10:10:21
Parser:	Cobertura
Assemblies:	2
Classes:	30
Files:	21
Line coverage:	87.7% (1825 of 2080)
Covered lines:	1825
Uncovered lines:	255
Coverable lines:	2080
Total lines:	5224
Branch coverage:	78.1% (1183 of 1513)
Covered branches:	1183
Total branches:	1513
Method coverage:	Feature is only available for sponsors

Coverage

Z3.Linq - 90.6%

Name	Line	Branch
Z3.Linq	90.6%	79.8%
Z3.Linq.BitVecWidthAttribute	80%	50%
Z3.Linq.ConstraintRef	100%
Z3.Linq.Environment	100%
Z3.Linq.Explanation	100%	100%
Z3.Linq.ExpressionVisitor	87.7%	72.9%
Z3.Linq.ExpressionVisitor.MarkerFinder	100%	100%
Z3.Linq.ExpressionVisitor.ParameterFinder	100%
Z3.Linq.MultipleEnvironment	100%
Z3.Linq.Rational	44.1%	58.3%
Z3.Linq.SolveableExtensions	100%	100%
Z3.Linq.Symbols	100%	66.6%
Z3.Linq.Theorem	93.6%	82.5%
Z3.Linq.Theorem.DeferredSolvable	100%
Z3.Linq.Theorem.ModelWitness	100%
Z3.Linq.Theorem<T, TResult>	93.6%	82.5%
Z3.Linq.Theorem	93.6%	82.5%
Z3.Linq.Theorem	93.3%	100%
Z3.Linq.TheoremGlobalRewriterAttribute	100%
Z3.Linq.TheoremPredicateRewriterAttribute	100%
Z3.Linq.TheoremUndecidedException	100%
Z3.Linq.TheoremVariableTypeMappingAttribute	0%
Z3.Linq.Z3Context	86.5%	92.8%
Z3.Linq.Z3Context.SolverParameter	33.3%	25%
Z3.Linq.Z3Methods	10%

Z3.Linq.Examples - 48.9%

Name	Line	Branch
Z3.Linq.Examples	48.9%	26%
Z3.Linq.Examples.RiverCrossing.MissionariesAndCannibals	87.5%	66.6%
Z3.Linq.Examples.Sudoku.SudokuGrid	0%	0%
Z3.Linq.Examples.Sudoku.SudokuGridTheorem	0%	0%
Z3.Linq.Examples.Sudoku.SudokuTable	0%	0%
Z3.Linq.Examples.Sudoku.SudokuTheorem	100%	100%
Z3.Linq.Examples.Sudoku.SudokuTheoremRewriter	100%

[github-actions]

Test Results

  1 files  ±0    1 suites  ±0   10s ⏱️ -3s
424 tests ±0  424 ✅ ±0  0 💤 ±0  0 ❌ ±0 
437 runs  ±0  437 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit d3eb6f2. ± Comparison against base commit 68a6356.

[jsboige]

[INFO] lane myia-po-2025:CoursIA — le seul rouge de cette tete est infra, pas de contenu.

Automerge & Label echoue a l'etape Generate token : Error: Input required and not supplied: app_id (run 40304942304, job 121511801388). C'est le workflow Dependabot du fork, qui attend les secrets d'une GitHub App absents sur ce depot ; il ne lit aucun fichier de la PR. Approve auto-mergeable dependabot PRs est skipped.

Les jambes de contenu sont vertes sur la tete d3eb6f24 : Compile & Analyse SUCCESS, build / Test SUCCESS, Package SUCCESS, Test Results SUCCESS (424 tests, 437 runs, 0 echec).

Rien a corriger cote diff ; les points restants sont la review et le merge.