Add(benchmarks,#18770): consolidate the Z3.Linq benchmark suite and its net8/net10 baselines by jsboige · Pull Request #36 · MyIntelligenceAgency/Z3.Linq

jsboige · 2026-10-23T16:50:57Z

Grain: DEEP/research-code — lane myia-po-2023:CoursIA — prev: LIGHT/ledger #14769

Objectif

Porter la suite de bancs BenchmarkDotNet de Z3.Linq dans le projet canonique de la
solution, après le port de main vers Z3 5.1.0 (#44), et publier les baselines
mesurées sur la pile courante. Quatrième pilier de la famille de bancs CoursIA
#18770, fille de l'EPIC .NET 11 #18695 : MetaGeneticSharp, Automata et SemanticFleet
ont déjà leur baseline.

See CoursIA #18770.

Pile déclarée

Cette branche intègre feature/bench-baseline (PR #46) par le commit de fusion
31c3ac5, et empile #36 dessus. #46 reste ouverte : cette PR ne la merge pas et ne
l'approuve pas. La comparaison multi-runtime est dans la PR empilée #47, dont la
base est cette branche.

Ce qui change

La suite étendue est consolidée dans solutions/Z3.Linq.Benchmarks, projet déjà
référencé par solutions/Z3.Linq.slnx : plus de projet benchmarks/ séparé, donc
plus de chemin de build hors solution.
PipelineConfig.cs porte le protocole de la famille : InProcessEmitToolchain,
InvocationCount=1, UnrollFactor=1, 5 warmup / 15 itérations. Sous
DOTNET_MULTI_RUNTIME=1, la configuration n'ajoute aucun job et laisse
BenchmarkDotNet produire les jambes runtime.
TheoremPipelineBenchmarks couvre le pipeline complet (contexte, réécriture de
l'arbre, AST Z3, solve, extraction du modèle) sur quatre charges : booléens
anonymes, entiers anonymes, réels via Symbols<double,double>, cinq variables via
Symbols<int×5>.
RationalBenchmarks couvre les quatre chemins publics de la constante : réduction
à la construction, égalité sur paires réduites, comparaison contre double,
émission de littéraux. Les données sont générées par un RNG seedé (Seed = 7).
Les baselines net8/net10 de SolveBenchmarks (PR bench(baseline): publish net8.0/net10.0 baselines for the solve suite (CoursIA #18770) #46) restent en place ; le corpus
étendu est documenté dans
BASELINE-extended-net8.0.md.

Correction de deux affirmations devenues fausses

La version antérieure de ce corps décrivait deux gaps de matérialisation à la tête
8a2562d. Ils ne sont plus vrais à cette tête et ne sont pas réutilisés :

ValueTuple — le chemin est exercé par SolveBenchmarks.ValueTuple et mesuré.
Type anonyme à membres double — GetSolution route désormais les types
anonymes par le même marshaller ConvertZ3Expression que les environnements
nommés ; la branche limitée à bool/int n'existe plus.

Aucun « gap » n'est donc déclaré ici sans une mesure qui le montre. Le chemin réel du
problème d'achat pétrolier reste Symbols<double,double>, qui nomme les variables ;
c'est ce que mesure la charge correspondante, et non une limite de l'API.

Baseline étendue — .NET 8.0 (moyennes)

Environnement : .NET 8.0.33 (8.0.3326.52219), SDK 10.0.114, BenchmarkDotNet 0.15.8,
InProcess 5/15, Intel Core i7-12700H 2.70 GHz, Windows 11 10.0.26300.9711.

Charge	Moyenne	Error (IC 99,9 %)	Alloué
`Solve bool pair`	9,960 ms	± 1,401 ms	7,23 KB
`Solve ints`	16,099 ms	± 2,053 ms	18,09 KB
`Solve reals (oil purchase)`	11,320 ms	± 1,740 ms	18,08 KB
`Solve Symbols 5 vars`	11,700 ms	± 2,043 ms	16,09 KB
`Rational.Of`	1,707 µs	± 0,439 µs	—
`Rational Equals`	5,887 µs	± 0,534 µs	—
`Rational compare vs double`	2,783 µs	± 0,474 µs	—
`Rational.ToString`	9,807 µs	± 2,088 µs	600 B

Les six formes de SolveBenchmarks sont dans le document de baseline, avec les mêmes
colonnes.

Les chiffres antérieurs à cette consolidation sont invalidés. L'ancienne table
annonçait quatre pipelines à ~35 ms : ces valeurs venaient de la bibliothèque avant le
port vers Z3 5.1.0, et les mêmes sources donnent 9,96 à 16,10 ms sur la pile courante.
Aucune valeur n'est ré-étiquetée.

Limites de mesure

MinIterationTime est signalé sur les quatorze charges : les itérations sont sous le
seuil recommandé de 100 ms.
Distribution multimodale signalée sur ValueTuple, WideSymbols, Solve bool pair,
Solve ints et Solve Symbols 5 vars. Tout écart inférieur à l'Error de sa ligne
est déclaré non-résultat.
Un tiret dans Allocated signifie « non observé », jamais « zéro octet garanti ».

Validation

dotnet build solutions/Z3.Linq.slnx -c Release : 0 warning, 0 erreur.
Tests via Microsoft.Testing.Platform (VSTest échoue sur le SDK .NET 10) :
solutions/Z3.Linq.Tests/bin/Release/net10.0/Z3.Linq.Tests.exe --progress off
→ 437 réussis, 0 échec, 0 ignoré.
Les logs des runs net8 et net10 sont conservés hors dépôt ; les valeurs publiées
viennent de ces logs, pas d'une reprise de mémoire.

Notes de revue

Aucune modification de la bibliothèque : le diff touche le projet de bancs, ses
documents de baseline et les deux README.
Le warning CS8603 sur Solve() (retour nullable sur unsat) est attendu : les
théorèmes mesurés sont satisfiables.
La PR Add(benchmarks,#18770): measure the fourteen charges on .NET 9/10/11 #47 ajoute les jambes .NET 9/10/11 RC sur le même corpus, avec la méthode par
racine runtime isolée — pas --runtimes, qui ne sait pas cibler le moniker du SDK
11 RC.

🤖 Generated with Claude Code

…IC #18695) benchmarks/Z3Linq.Benchmarks: 4 theorem-pipeline benchmarks (anonymous bool/int, Symbols int/real, per-Solve full pipeline) + 4 Rational micro-benchmarks (public API surface only), InProcessEmitToolchain + Job.ShortRun, net8.0 baseline TFM. benchmarks/BASELINE-net8.0.md: environment table + results + hot path reading + the two materialization gaps measured at 8a2562d (ValueTuple ctor-name Ordinal mismatch crashing the repo's own demo; anonymous double not dispatched). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

jsboige · 2026-10-23T16:51:09Z

Findings tracking: the two materialization gaps documented in BASELINE-net8.0.md are reported in #35.

github-actions · 2026-10-23T16:55:41Z

Test Results

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

Results for commit 7509c8c. ± Comparison against base commit 0f00539.

♻️ This comment has been updated with latest results.

jsboige · 2026-10-24T04:54:35Z

[note de lane] Les checks rouges de cette PR ne viennent pas de son diff. Diagnostique ce cycle :

Automerge & Label echoue sur toutes les PRs du depot — ##[error]Error: Input required and not supplied: app_id (tibdex/github-app-token) : le depot ne porte pas les secrets d'application. Aucun commit de PR ne peut le faire passer.
build / Package (le cas echeant) vient d'un flake de l'action tierce endjin/Endjin.RecommendedPractices.GitHubActions@main : Install-Package: No match was found ... 'Powershell-yaml'. Rejeu fait ; la reference mutable est le defaut durable.

build / Compile & Analyse, build / Test et Test Results sont verts sur cette PR.

Suivi ouvert : #41 (criteres d'acceptation : job silencieux quand le jeton est absent + epinglage par SHA).

@main

…lication Le job 'Automerge & Label' lancait l'etape 'Generate token' sans condition : sur un depot qui ne porte pas DEPENDJINBOT_APP_ID / DEPENDJINBOT_PRIVATE_KEY, l'etape echouait et TOUTES les PRs portaient un rouge qui ne dit rien de leur contenu (mesure : #36, #37, #38, #40 -- build vert, ce job FAILURE). Une etape de garde lit les deux secrets dans son env: -- le contexte secrets n'est pas disponible dans l'expression if: d'un job -- et publie app_credentials_available. L'etape de jeton et l'automerge la consomment ; l'etiquetage pending_release, qui n'utilise que GITHUB_TOKEN, continue de tourner. Garde absente = ::notice explicite dans les checks. Endjin.RecommendedPractices.GitHubActions est epingle par SHA (16b26fe, main du 2026-10-24) a ses deux references : l'action prepare-env-vars-and-secrets et le pipeline reusable scripted-build-pipeline.yml. @main est une reference mutable, et une de ses dependances a deja casse build / Package sur #40 sans qu'aucun commit du depot ne l'ait cause. See #41

jsboige · 2026-10-24T22:31:40Z

[ADJOINT PREFLIGHT] #36 — comparaison benchmark et preuves manquantes

Lane myia-po-2025:CoursIA-2 ; tête f860183. Avis COMMENTED : pas merge-ready. Recommandation de véhicule à ai-01 : #34 après corrections, en préservant les apports uniques de #36 avant une éventuelle clôture ; aucun arbitrage ni transfert effectué ici.

Lecture déléguée complète des surfaces des deux PRs (body, commentaires, reviews/inline/threads vides), diffs et CI exact-head, puis recoupement personnel des sources et logs. Six fichiers ajoutés, +264/-0. Les quatre pipelines et quatre microbancs Rational élargissent utilement la couverture de #34. Aucun build de cette branche ni rerun BDN effectué par le lecteur ou l'attestant : les résultats sont rapportés par l'auteur.

Défauts à traiter :

BenchConfig.cs annonce 5 warmups/15 itérations mais ne fait que AddJob(Job.ShortRun.WithToolchain(...).WithId(...)). La baseline dit elle-même 3/3. Le protocole décrit dans le body et le commentaire n'est donc pas celui des mesures. Fixer explicitement le protocole retenu puis refaire les mesures ; ne pas simplement réétiqueter les anciennes comme 5/15.
Le nouveau projet n'est pas dans solutions/Z3.Linq.sln et n'apparaît pas dans le log du check Compile & Analyse 120539743879 (Demo, Examples, Tests, bibliothèque seulement). Ce vert ne valide pas le code ajouté. Ajouter une compilation effective du banc à la CI ou une intégration solution compatible.
« Rational compare vs double » est documenté comme ZeroMeasurement (~0 ns) sur opérandes static readonly ; remplacer par des données non constantes/paramétrées et re-mesurer avant d'en faire une référence.
Les erreurs imprimées des quatre pipelines vont de 53 % à 192 % de leur moyenne. Elles ne justifient pas une conclusion de gain runtime ; stabiliser les mesures et limiter les interprétations. La cause « quasi intégralement natif + réflexion » n'est pas établie par ce seul tableau sans profilage.
Le texte « remplace pb-bench » ne correspond à aucune suppression ou migration du banc existant ; le qualifier comme nouvelle référence proposée. Aucun lien README ajouté : rendre la référence découvrable si ce véhicule est retenu.

CI exacte tête : onze checks, fold filter=all dernier (started_at,id) par nom ; Compile & Analyse, Test et Package success, mais avec la limite de couverture ci-dessus. Automerge & Label failure (app_id, suivi #41), état UNSTABLE. Les résultats de compilation/tests du dépôt ne sont pas des résultats BDN.

Apports à conserver : anonyme bool/int, réel Symbols<double,double>, arité cinq, réduction/égalité/comparaison/émission Rational. Les conserver ne signifie pas conserver les résultats invalidés ou la ZeroMeasurement. Aucun merge, fermeture, approbation, refresh ou push effectué. Gate CoursIA non applicable au fork ; ledger issue-debt N/A, entité PR.

…ouble, sln integration - BenchConfig: WithWarmupCount(5).WithIterationCount(15) explicit (ShortRun default is 3/3) - protocol announced in docstring now matches execution, aligned with MetaGeneticSharp#61 family canon. - Rational compare vs double: rewritten on seeded RNG data (Seed=7, GlobalSetup tables, 64 comparisons/iteration) - was a ZeroMeasurement on static readonly operands (JIT constant folding), review point 3. - Z3Linq.Benchmarks added to solutions/Z3.Linq.sln: Compile & Analyse now builds the bench project, review point 2. - README: Benchmarks section with link to BASELINE-net8.0.md (discoverability, review point 6). New proposed reference next to the existing pb-bench console (no removal claimed, review point 5). - Nullability warnings CS8603 x2 silenced with Solve()! (no IL change). Measurements re-run under the pinned protocol in the following baseline commit (old 3/3 table invalidated, not relabelled). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

…ned 5/15 protocol Full re-measurement at 84de65c (net8.0.33, SDK 10.0.114): pipeline errors drop from 53-192% to 3.6-5.5%, floor re-measured at 35.06 ms (previous 3/3 table invalidated, floor doubled), compare-vs-double now measured on seeded data (127.41 ns). Causal claim 'native + reflection' withdrawn - reading limited to what the tables carry. Positioned as proposed new reference next to pb-bench (no removal claimed). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

jsboige · 2026-10-26T23:27:36Z

Réponse au [ADJOINT PREFLIGHT] du 24/10 — les six défauts traités aux commits 84de65c6 (code) et 71aa39b (baseline), re-mesure complète, pas un ré-étiquetage.

Protocole annoncé vs exécuté — BenchConfig épingle désormais .WithWarmupCount(5).WithIterationCount(15) (le Job.ShortRun nu est 3/3 ; canon famille MetaGeneticSharp#61), et la docstring nomme BenchConfig.cs + la baseline comme sources du protocole. Toutes les mesures de BASELINE-net8.0.md ont été refaites sous ce protocole 5/15 — aucun chiffre de l'ancienne table 3/3 n'est réutilisé.
Banc absent de la solution — Z3Linq.Benchmarks.csproj est le 5e projet de solutions/Z3.Linq.sln. Compile & Analyse compilera le banc à chaque PR ; build solution complet vérifié local (0 erreur, 0 warning).
compare vs double ZeroMeasurement — banc réécrit sur données non constantes : GlobalSetup génère 32 Rational + 32 seuils double par RNG seedé (Seed = 7, pattern famille), 64 comparaisons par itération sur tableaux. Re-mesuré : 127,41 ns ± 4,225 ns (3,3 %) — plus d'élimination JIT, le chemin opérateur est mesuré (~2 ns/comparaison).
Erreurs 53-192 % et interprétation — sous 5 warmup / 15 itérations, les erreurs pipeline passent à 3,6-5,5 % (35,06 ms ± 5,5 % · 36,54 ms ± 5,3 % · 36,73 ms ± 5,2 % · 37,12 ms ± 3,6 %). Conséquence honnête : le plancher re-mesuré double l'ancienne valeur (15,5 → 35,1 ms) — l'ancienne table 3/3 est invalidée, la nouvelle est la référence. La causalité « quasi intégralement natif + réflexion » est retirée de la baseline ; la lecture se limite à ce que les tables portent (plancher, croissance ≤ 6 % sur la gamme, allocations 6-18 KB, répartition natif/managé non conclue sans profilage).
« Remplace le banc console brut pb-bench » — reformulé dans la baseline : le banc BDN est une nouvelle référence proposée à côté du banc console existant (aucune suppression ni migration n'accompagne cette PR).
Découvrabilité README — section ## Benchmarks ajoutée : ce que le banc exerce, commande de lancement, lien vers benchmarks/BASELINE-net8.0.md.

Apports conservés tels quels (anonyme bool/int, Symbols<double,double> réel, arité cinq, réduction/égalité/comparaison/émission Rational) ; les résultats invalidés (ZeroMeasurement, table 3/3) sont remplacés par la re-mesure, pas conservés. Warnings nullability CS8603 ×2 du projet banc éliminés au même commit (annotation seule, aucun changement d'IL mesuré).

Grain: MED/research-code — lane myia-po-2023:CoursIA — prev: LIGHT/guard #22799

… (CoursIA #18770) Align the suite on the family protocol (InProcessEmitToolchain, ShortRun, InvocationCount=1, UnrollFactor=1, 5 warmup / 15 iterations, guarded by DOTNET_MULTI_RUNTIME=1 for multi-runtime delta runs), multi-target the benchmarks project to net8.0;net10.0 to follow the library, and record the reference runs as BASELINE-net8.0.md / BASELINE-net10.0.md (same protocol as MetaGeneticSharp .NET 9 and Automata .NET 8/9). Point the suite README at them. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

Carry the extended pipeline and Rational benchmarks onto the .slnx solution and the compatible net8/net10 baseline. The existing benchmark project is already registered in the solution. Co-Authored-By: Kimi <noreply@moonshot.cn>

Move the extended theorem-pipeline and Rational benchmarks into the canonical solutions/Z3.Linq.Benchmarks project from main, so the suite builds against the current library and Z3 5.1.0 instead of the removed standalone project. Add a same-machine net8 baseline for the 14 extended charges, refresh the stale documentation links, and remove the inaccurate claims about ValueTuple and anonymous-type materialisation. Validation: dotnet build solutions/Z3.Linq.slnx -c Release (0 warnings, 0 errors); MTP suite 437/437 passed. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

The canonical solutions/Z3.Linq.Benchmarks project carries its own Program.cs. Keeping the old benchmarks/Z3Linq.Benchmarks/Program.cs left a tracked file whose project no longer exists and which the solution never compiles. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

jsboige · 2026-10-27T01:16:22Z

Réponse au [ADJOINT PREFLIGHT] du 24/10, à la tête e664ece. Le corps de la PR a été réécrit : il ne décrit plus l'ancienne arborescence, et la réponse du 26/10 est superseded — ses valeurs ~35 ms venaient de la bibliothèque avant le port de main vers Z3 5.1.0 (#44). Les chiffres publiés aujourd'hui sont une re-mesure sur la pile courante, pas un ré-étiquetage.

Protocole annoncé vs exécuté — solutions/Z3.Linq.Benchmarks/PipelineConfig.cs épingle explicitement InProcessEmitToolchain, InvocationCount=1, UnrollFactor=1, WithWarmupCount(5), WithIterationCount(15). Les quatorze charges ont été mesurées sous ce protocole après la consolidation. Le corps publie ce protocole et les Error de chaque ligne.
Banc absent de la solution — le projet est désormais solutions/Z3.Linq.Benchmarks/Z3.Linq.Benchmarks.csproj, référencé par solutions/Z3.Linq.slnx (ligne 14). dotnet build solutions/Z3.Linq.slnx -c Release : 0 warning, 0 erreur. Le check Compile & Analyse de cette tête est relancé et était encore IN_PROGRESS au moment de ce commentaire ; je ne le déclare pas vert.
compare vs double ZeroMeasurement — corrigé avant cette tête : GlobalSetup génère 32 Rational et 32 seuils double par RNG seedé (Seed = 7), 64 comparaisons par itération. Mesure courante : 2,783 µs ± 0,474 µs. Aucune mesure à ~0 ns n'est publiée.
Erreurs et interprétation — les erreurs des quatre pipelines sont maintenant de 12,8 % à 17,5 % de leur moyenne (1,401 à 2,053 ms), et non plus 53-192 %. MinIterationTime reste signalé sur les quatorze charges et plusieurs distributions sont multimodales : le corps le dit, et cette PR ne revendique aucun gain runtime. La PR Add(benchmarks,#18770): measure the fourteen charges on .NET 9/10/11 #47 (empilée sur celle-ci) documente les jambes .NET 9/10/11 RC comme un run unique par runtime, avec tout delta inférieur à son Error déclaré non-résultat; l'attribution JIT / solveur natif / bruit n'est pas tranchée.
« Remplace pb-bench » — le texte a disparu. Le corps présente le banc comme une nouvelle référence proposée; aucune suppression du banc console existant n'est revendiquée. Le Program.cs retiré par e664ece est l'entrée du projet de banc ajouté par bench(baseline): publish net8.0/net10.0 baselines for the solve suite (CoursIA #18770) #46, remplacée par le projet solutions/, pas le banc pb-bench.
Découvrabilité README — README.md et solutions/Z3.Linq.Benchmarks/README.md pointent vers le projet canonique et les documents de baseline; la section ## Benchmarks donne la commande de lancement.

La pile reste déclarée : cette branche intègre feature/bench-baseline (#46) par le commit de fusion 31c3ac5; #46 reste ouverte et n'est ni mergée ni approuvée par cette PR. La comparaison multi-runtime est dans #47, dont la base est cette branche.

Repeated the six-benchmark suite on both TFMs, same machine, same protocol (InProcessEmitToolchain, ShortRun, InvocationCount=1). Allocations per solve are stable to within 3% across runs (6.09 KB identical on ScalarSymbols) and rise on every shape under .NET 10 in both runs (+37% to +101%), so the allocation regression is a measured fact. Means are not: net8's own Mean moves -32% to -4% between the two runs (ScalarSymbols 17.04 -> 11.67 ms, NestedObject 14.42 -> 9.65 ms), an amplitude larger than the cross-TFM delta, and every RatioSD (0.14 to 0.20) spans 1.0. The earlier "-32% Mean on .NET 10" does not survive repetition; both files now say so instead of carrying a single-run observation. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

…on drives Allocated Third run of the same six-shape suite on the same machine and protocol, plus a four-leg cross-check isolating the runtime from the compilation target. Findings: - The compilation target is not the factor. The net8.0 binary under .NET 10 and the net10.0 binary under .NET 10 agree on five of six shapes; the net8.0 -> .NET 10 delta (+1.64 KB on ScalarSymbols, +37 % to +95 % over the six shapes) is a runtime effect. - The published net8.0 baseline reproduces to the kilobyte on five of six shapes; Optimize moves 6.55 -> 5.94 KB (-9.3 %). The "+/-3 %" noise claim announced with the second run was too tight and is corrected here. - Allocated is not a property of the charge. The same charge, same binary and same runtime allocates 6.42 KB when only the six Solve charges run and 13.59 KB when the Rational charges run in the same process. Removing the Rational class removes the amplification entirely (13.59 -> 6.42 KB); removing the TheoremPipeline class does not (6.42 KB either way). Two published baselines are therefore comparable only when the process composition is held constant. - The Mean is not reproducible: the same leg measured 17.04, 11.67 and 24.49 ms over three runs (x2.1), an amplitude of the same order as the cross-runtime deltas the family compares. The within-run Error does not bound it. New file BASELINE-runtime-crosscheck.md holds the protocol, the tables, the class-removal bisect and the reproduction commands. The two baseline files now point at it and carry the corrected noise figure. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

…osition effect The trigger is established and reproducible (the Rational charge class executing in the same process), but the mechanism proposed with the previous commit is falsified by the source: Rational is a purely managed readonly struct (two longs, GCD reduction) and RationalBenchmarks calls no Z3 context, no AST and no native function. The amplifying charges never touch the solver, so a solver-side state cannot explain their effect on the measured allocation of the solver charges. The document now states the falsification instead of the hypothesis, and frames the open question that actually matters for the family: whether the Allocated column measured in-process is a property of the charge or of the process. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>

Base refresh: #46 advanced after this branch forked (36fad90 + c759c69 -- third run, runtime cross-check document, dropped falsified mechanism hypothesis). Documentary push, no content conflict expected (verified by merge-tree dry-run).

…lti-runtime Base refresh (#36 -> #47): brings in #46's runtime cross-check document and the base-merge of feature/bench-baseline into #36.

github-actions · 2026-10-29T14:05:24Z

Code Coverage Summary Report - Linux (No TFM)

Summary


Generated on:	10/29/2026 - 14:05: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.3%	100%
Z3.Linq.Theorem	93.6%	82.5%
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%

jsboige mentioned this pull request Oct 23, 2026

[P1] .NET 11 EPIC #18695 -- banc BenchmarkDotNet in-repo par sous-module (baseline net8/net9) jsboige/CoursIA#18770

Open

3 tasks

jsboige mentioned this pull request Oct 24, 2026

CI: approve_and_label echoue sur TOUTES les PRs (app_id absent) et une action tierce @main casse build/Package #41

Open

3 tasks

This was referenced Oct 24, 2026

CI inerte : 0 run depuis toujours (3 workflows actifs, Actions enabled) — #20 afficherait CLEAN sans avoir jamais compile #23

Open

CI: pull_request trigger declared but never fires - PRs get no checks (all 6 runs are workflow_dispatch) #30

Open

This was referenced Oct 24, 2026

Fix(ci,#41): Automerge & Label ne rougit plus sans identifiants d'application #42

Open

feat(benchmarks): BenchmarkDotNet baseline suite (.NET 9) for public theorem API #34

Open

jsboigeEpita and others added 2 commits October 27, 2026 00:26

jsboige and others added 4 commits October 27, 2026 01:34

jsboige mentioned this pull request Oct 27, 2026

Add(benchmarks,#18770): measure the fourteen charges on .NET 9/10/11 #47

Open

jsboige changed the title ~~Add BenchmarkDotNet baseline for Z3.Linq (net8.0, CoursIA #18770)~~ Add(benchmarks,#18770): consolidate the Z3.Linq benchmark suite and its net8/net10 baselines Oct 27, 2026

jsboige and others added 4 commits October 27, 2026 02:34

jsboige pushed a commit that referenced this pull request Oct 29, 2026

Merge branch 'bench/18770-z3linq-baseline' into bench/18770-z3linq-mu…

4e9b07e

…lti-runtime Base refresh (#36 -> #47): brings in #46's runtime cross-check document and the base-merge of feature/bench-baseline into #36.

Navigation Menu

Repository navigation

Add(benchmarks,#18770): consolidate the Z3.Linq benchmark suite and its net8/net10 baselines - #36

Add(benchmarks,#18770): consolidate the Z3.Linq benchmark suite and its net8/net10 baselines#36
jsboige wants to merge 11 commits into
mainfrom
bench/18770-z3linq-baseline

jsboige commented Oct 23, 2026 •

edited

Loading

Uh oh!

jsboige commented Oct 23, 2026

Uh oh!

github-actions Bot commented Oct 23, 2026 •

edited

Loading

Uh oh!

jsboige commented Oct 24, 2026

Uh oh!

jsboige commented Oct 24, 2026

Uh oh!

jsboige commented Oct 26, 2026

Uh oh!

jsboige commented Oct 27, 2026

Uh oh!

github-actions Bot commented Oct 29, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

jsboige commented Oct 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Objectif

Pile déclarée

Ce qui change

Correction de deux affirmations devenues fausses

Baseline étendue — .NET 8.0 (moyennes)

Limites de mesure

Validation

Notes de revue

Uh oh!

jsboige commented Oct 23, 2026

Uh oh!

github-actions Bot commented Oct 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Test Results

Uh oh!

jsboige commented Oct 24, 2026

Uh oh!

jsboige commented Oct 24, 2026

Uh oh!

jsboige commented Oct 26, 2026

Uh oh!

jsboige commented Oct 27, 2026

Uh oh!

github-actions Bot commented Oct 29, 2026

Code Coverage Summary Report - Linux (No TFM)

Coverage

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jsboige commented Oct 23, 2026 •

edited

Loading

github-actions Bot commented Oct 23, 2026 •

edited

Loading