SFAz3 models seem to have max length 21 characters

[jsboige]

A simple repro: In Automata.Z3.Tests in FiniteAutomataTests.cs#L510, change \d{3} for \d{22} and the test should fail with a valid string truncated for the first 21 chars.

Tests with other longer repetitions yielded the same behavior.

Furthermore, trying to upgrade Z3 NuGet dependency from 4.5 to version 4.8.1, (more recent versions don't seem to like the targeted Framework 4.5), a couple tests won't pass anymore. The one above then fails with an empty model.

[jsboige]

Boucle bouclée — six ans après

Ce ticket a été résolu côté fork MyIntelligenceAgency/Automata (PR #1 mergée localement), et end-to-end dans la série CoursIA via EPIC #2979.

Diagnostic vérifié

Le plafond « 21 chars » n'était pas une borne fondamentale du moteur de witness. C'était une NullReferenceException dans BDDAlgebra.Choose, causée par un mismatch d'identité de terminal BDD entre deux solveurs : RexEngine(BitWidth) construit son propre CharSetSolver interne, alors que l'automate est bâti par l'appelant avec un CharSetSolver séparé. Les BDD d'étiquettes de transition appartiennent à l'algèbre de l'appelant ; la descente Choose compare aux terminaux True/False du solveur du moteur (identités d'objet distinctes), n'atteint jamais un terminal, suit un enfant null → déréférence. Les « 21 chars » étaient l'endroit où la marche divergente plantait.

Fix (commit 9e1fb28)

Garde d'identité d'algèbre en tête de RexEngine.GenerateMember. Test fork GenerateMember_WitnessOver21Chars_CapIsLifted : [a-z]{22} produit un témoin ≥ 22 caractères ✅.

Livraison CoursIA (boucle complète, tous MERGED)

PR CoursIA	Scope
#3072	NB-06 témoin A & ~B + Sudoku-13 §6b consomment &/~ fork
#3130	NB-06 ferme la boucle emit→solve SMT-LIB 2.6 + Z3
#3140	Sudoku-13 livré (49 cellules, 4×4 + 9×9 via 2-à-2)

Notebooks consommateurs

• MyIA.AI.Notebooks/SymbolicAI/SMT/Z3/10_Witness_Generation_Automata.ipynb (32 cellules, 16 code) — démontre &/~ + witness + Z3 SMT-LIB 2.6 + cap 21-char levé.
• MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-Csharp.ipynb (49 cellules, 18 code) — barreau 2 (BREX/Rex) + barreau 3 (RE# vérifie) + barreau 4 (Z3 résout 9×9).

Caveats honnêtes

• 49 tests legacy Automata.Tests échouent (dette pré-existante modernisation net8 : sérialisation BinaryFormatter SYSLIB0011 obsolète, CodeGen C++/C# DLL externes). Aucune régression liée à ce fix ; les tests #2979 sont TOUS verts.
• Le fork MyIntelligenceAgency/Automata a déjà fusionné upstream master (commit 3f6baaa) mais le PR upstream AutomataDotNet/Automata n'a pas encore été posté. Créneau calme à venir.

Le ticket peut être marqué CLOSED côté upstream si la modération le souhaite, ou laissé OPEN pour traçabilité jusqu'à la PR upstream formelle. Voir Epic #2978 / #2979 côté CoursIA pour le contexte.

— myia-po-2025 (CoursIA-2), 2026-07-03, six ans pile après l'ouverture initiale (2020).