Page-by-page review, 2 October 2026

Page-by-page review, 2 October 2026#

This review covers the 84 pages in the current manual at 8c76deb. The historical book is a reference for preservation, not a second current manual. The writer applies corrections and separate read-only reviewers check the pages and revisions against the review checklist.

This record separates technical review from reader acceptance and solver qualification. It does not renew old benchmark or fuzzing evidence.

Page coverage#

Every baseline page was read in full by an independent reviewer. “Corrected” means that this review changed the page, including explicit qualifications where implementation work remains open. “No required edits” means no required repair was identified within the stated review scope; neither verdict certifies solver correctness. Finding IDs are summarized below. R-001 covers historical migration wording corrected by the writer and checked by reviewer I; R-002 is this review’s status update, also checked separately.

The 84-page baseline excludes this newly added review record.

Introduction#

Page	Review outcome	Findings
Primo	No required edits	—

Using Primo#

Page	Review outcome	Findings
Supported input and capabilities	No required edits	—
Build and run Primo	No required edits	—
SMT-LIB input and results	Corrected	A-009
Request a model	No required edits	—
Repeated queries and scopes	No required edits	—

Reference#

Page	Review outcome	Findings
Command-line options and output	Corrected	A-001; A-012/A-013 closed with SLURM evidence
Effective policies and option dependencies	Corrected	A-004, A-010
Tactic reference	Corrected	A-008
Statistics reference	Corrected	A-001, A-003, A-005–A-007, A-011
SAT backend operations	Corrected	A-002

Contributing#

Page	Review outcome	Findings
Correctness before performance	Corrected	B-004, B-006, B-010
Contributing an implementation change	No required edits	—
Fuzzing and reducing failures	Corrected	B-005, B-009
Independent model and session validation	Corrected	B-001, B-003
Debugging and investigating regressions	No required edits	—
Reproducible experiments	Corrected	B-002, B-004, B-010; B-012/B-013 closed
Tuning an existing configuration	Corrected	B-014 repaired and qualified
Writing and checking documentation	Corrected	B-007

Understanding Primo#

Page	Review outcome	Findings
From commands to an answer	No required edits	—
Terms, symbols, and ownership	Corrected	C-002
Frontend: syntax, names, and typed terms	No required edits	—
Sessions: scopes, replay, and retained engines	No required edits	—
Goals, tactics, and strategies	Corrected	C-001, C-003; C-004 closed
Preprocessing	Corrected	D-001–D-005; D-006 resolved below
Boolean abstraction and SAT integration	No required edits	—
DPLL(T): connecting Boolean search and theory reasoning	No required edits	—
EUF: congruence, explanations, and rollback	No required edits	—
Linear real arithmetic	Corrected	E-001–E-003
Linear integer arithmetic	No required edits	—
Theory combination	Corrected	F-001
Quantifiers: binders and instantiation	Corrected	F-002
Models: values, function tables, and reconstruction	Corrected	F-003

Literature#

Page	Review outcome	Findings
Literature and implementation mapping	No required edits	—
Bibliography	No required edits	—
Reported QF_LRA results	No required edits	—
Bromberger: integer search, cubes and preprocessing	No required edits	—
Integer-model repair and MIP primal heuristics	No required edits	—
Yices: architecture, dynamic Ackermannization, and lemma reuse	Corrected	G-002
Clause forgetting: correctness and termination	Corrected	G-001
Polarity-aware CNF in SMT	No required edits	—
Don’t-care reasoning and relevance	Corrected	G-003

Open leads#

Page	Review outcome	Findings
Research register	Corrected	H-001; C-004 closed
Library API and embedding	No required edits	—
Incremental memory and reference counting	No required edits	—
Compact term storage and future payloads	No required edits	—
Compact rational storage	Corrected	H-003
Statistics instrumentation and build profiles	No required edits	—
Dynamic Ackermannization and theory-lemma retention	No required edits	—
Safe forgetting of theory lemmas	No required edits	—
Floating-point-guided LRA basis selection	Corrected	H-003
Complete implied-equality basis	No required edits	—
GCD reasoning with bounded variables	Corrected	H-002, H-003
Configurable and better-guided integer patching	Corrected	H-003, H-006
Avoiding infinitesimals in integer relaxation	No required edits	—
More selective and cheaper care-pair generation	No required edits	—
Reducing combination obligations with care graphs	No required edits	—
Move QF_UFLRA to the general component driver	No required edits	—
Further model-based combination transitions	No required edits	—
Quantifier instantiation efficiency	No required edits	—
Optional NNF through quantifiers	Corrected	H-003
Exploiting directly asserted quantifiers	Corrected	H-003
Skipping irrelevant quantified obligations	Corrected	H-003
Compact handling of large distinct assertions	Corrected	H-002, H-004, H-005
Equation elimination across queries	Corrected	H-002, H-004, H-005
Sharing immutable EUF preparation between checks	Corrected	H-002, H-005

Active work#

Page	Review outcome	Findings
Public launch preparation	Corrected	B-008; D-006 resolved below
GitHub publication handoff	Corrected	B-008; D-006 resolved below
Documentation replacement	Corrected	B-007
Evidence work still open	Corrected	B-011
Results storage	Corrected	B-010

Evidence and history#

Page	Review outcome	Findings
Publication qualification	Corrected	I-002
Assignment migration evidence	No required edits	—
Arithmetic engineering and retained evidence	No required edits	—
Quantifier decisions and checking evidence	No required edits	—
Retained documentation and evidence	Corrected	R-001
Historical documentation review	Corrected	R-001

Documentation review#

Page	Review outcome	Findings
Documentation closing review	Corrected	R-002; D-006 resolved below
Preservation audit	Corrected	R-001
Frontend and session preservation map	No required edits	—
Solver chapter preservation map	No required edits	—
Integer-arithmetic preservation map	Corrected	R-001
Tactics and preprocessing preservation map	Corrected	I-001, I-003
Guides, practice, literature, and leads	Corrected	R-001

Corrections and independent review#

Six read-only reviewers covered nine groups; the writer applied the changes. Each revised group returned to its original reviewer. The following summary records the required repairs and accepted suggestions, not just broken links. The source findings and their current dispositions are recorded below.

Group and reviewer	Findings and disposition
A — Hilbert; guides and reference	A-001–A-011: correct conflict-budget coverage, backend range handling, counter/default claims, traversal cost, timer boundaries, model examples, cancellation behavior, input navigation and paper/source links. A-012/A-013 are now repaired and qualified below.
B — Kierkegaard; contributor guides and active work	B-001–B-011: use SAT-only model-validation inputs, describe analyzer limits, supply retained-session recipes, preserve the maintainer execution policy, qualify seed-size bounds, repair source selections and link the current ledger. B-012–B-014 are now repaired and qualified below.
C — Averroes; core, frontend, sessions and tactics	C-001–C-003: distinguish strategy labels from callable behavior, typed-model ownership from printed text, and correct implementation links. C-004 is now repaired and qualified below.
D — Herschel; preprocessing, SAT, DPLL(T) and EUF	D-001–D-005: describe joint bounded Gauss–Jordan elimination, enabled ITE distribution, appended simplification consequences, passive result storage and the correct equality rewrite. D-006 was independently cross-checked by Avicenna; the subsequent repair and qualification are recorded below.
E — Avicenna; arithmetic	E-001–E-003: assign phase-refresh tracking to the online propagator and link the editable figure and actual rational fields. No required LIA chapter edits.
F — Kuhn; combination, quantifiers and models	F-001–F-003: retain conservative unmapped-pair fallback, distinguish propositional from equality-dependent test coverage, and select the complete model lookup.
G — Averroes; literature	G-001–G-003: include the clause-forgetting correctness section and select the actual Ackermann evidence and arithmetic relevance lead.
H — Kierkegaard; open leads	H-001–H-006: classify conflict generalization as implemented, repair historical selections, separate contributor machine choice from maintainer policy, restore mandatory fuzz/model gates, link current owners and define the delta-aware floor.
I — Kuhn; evidence and preservation	I-001–I-003: describe the completed archive migration, identify the historical reproducibility-tool revisions and link tactic counters to their actual reference. R-001/R-002 preserve the distinction between historical reviews, this technical review and reader/publication acceptance.

Verification and limits#

The review compared claims with owning headers, implementations, callers, option defaults and selected test bodies. It checked mathematical examples, implementation status, paper attribution, source-link destinations and the separation of architecture, procedures and evidence. Reading a test body is not evidence that the test passed at this revision.

Primary reading included the relevant EUF and arithmetic mechanisms, theory combination and quantifier distinctions, the strategy paper, Bromberger’s thesis selections, the MIP heuristic survey sources, Yices, clause-forgetting conditions, polarity/relevance papers, IPASIR-UP and symmetry preconditions. The published Primo tables were checked for transcription. This was not a new proof audit of every citation or every paper section in the bibliography. The original Plaisted–Greenbaum full text remains unavailable; its literature page states that limit and identifies the primary modern account actually used.

During the original documentation review, no solver, test suite, fuzzing campaign or benchmark was run. The subsequent D-006 qualification is recorded separately below. Existing qualification records were inspected without renewing them; raw experiment archives were not exhaustively reaggregated. Changed validation recipes were checked against their tools, not executed as fresh qualification. Historical pages were checked for preservation and link routing, not rewritten or newly certified as current implementation descriptions. Repository visibility, hosted settings, deployment, legal rights and the absence of secrets were not certified by this documentation review.

make docs-check-links passed the full strict build of both books and the assembled-site check: 255 HTML pages, 30,993 local links, 948 unique Git links and zero local/Git failures. The assembler retained 1,306 historical targets, 75 redirect pages and 91 fragment routes. Browser checks at the /primo/ project prefix covered all 85 current pages, including this new record, and 557 rendered math containers after font loading. They found no unrendered equations, MathJax errors, page-width overflow or Sphinx error nodes. Selected changed sections were also inspected visually. This is a desktop check, not an exhaustive mobile or accessibility audit.

External-host results are a separate dated observation: the current book had four failed targets and two timeouts; the historical book had thirteen failed targets and two timeouts. See the full external-link report for exact URLs, commands and access errors. These failures remain visible.

Correctness follow-ups#

These findings originated in source inspection. D-006 has since been reproduced, repaired and qualified on SLURM. The six supporting-tool and resource-control findings are also repaired and qualified; their implementation regressions and fresh SLURM evidence are recorded below.

D-006: symmetry comparison omits numeric payloads#

Resolved: reproduced on the reviewed solver, repaired and qualified on SLURM.

The reviewed symmetry comparison key included term kind, sort, symbol, Boolean value and children, but omitted rational_value. Numeric literals and multiplication coefficients use that payload. Consequently the key can identify different arithmetic expressions, invalidating the permutation-invariance test used by UfSymmetryBreaker.

The numeric-value regression has distinct uninterpreted values c0, c1, a fresh constant t restricted to those values, and a function h to Real. Create c0 before c1 so that its TermId is smaller:

distinct(c0, c1)
t = c0 or t = c1
h(c0) = 0
h(c1) = 1
h(t) = 1

There is a model with t = c1. Swapping c0 and c1 does not preserve these assertions, but a key that identifies numeric 0 with 1 can accept that swap. The faulty value-precedence path adds not(t = c1) for the first fixed term t, removing the satisfying choice. Two independent source reviews traced the faulty insertion, including the supported --preprocessing-mode=basic --preprocessing-passes=0 path.

The old solver at 09749dd returned UNSAT for this satisfiable input under both default preprocessing and Basic with zero rounds. A second regression uses different multiplication coefficients and exposes the same false answer. Z3, cvc5 and Primo with symmetry breaking disabled returned SAT for both.

Regression	Old default	Repaired default	Z3 and cvc5
Different numerals	UNSAT (wrong)	SAT	SAT
Different coefficients	UNSAT (wrong)	SAT	SAT
Equal-payload control	SAT	SAT	SAT

The two failures also occur with Basic zero-round preprocessing and value precedence disabled. The repaired solver returns SAT in all four CLI profiles: default, Basic zero-round, Basic zero-round without value precedence, and Basic zero-round without symmetry breaking. Dolmen accepts all twelve resulting models. Reference comparison is necessary here: model validation alone would not detect a false UNSAT answer.

The repair preserves the exact rational payload for every node, including Rational, Times, IntDiv and IntMod. The design checklist follows Déharbe et al., §3, Definitions 2–4, Theorem 5 and Lemma 6 [22]: equality of comparison keys must imply identical syntax after sort-preserving constant renaming and the permitted commutative reordering. It must not erase interpreted arithmetic values. General symmetry detection and a new value-precedence algorithm are outside this repair.

The regression coverage checks unequal numeric payloads, signs, fractions, large values, coefficients and divisors; equal-payload controls must still admit symmetry. Both restriction modes are covered. The three SMT-LIB regressions exercise default preprocessing, Basic with zero rounds and symmetry disabled: 40 direct-pass calls and 18 solver assertions, including equal-payload controls.

Qualification used the repaired snapshot a953edd. All 43 release CTest targets, 216 Python tests, 12 documentation examples and all 43 ASan CTest targets passed. The fresh differential gate passed 3,000 general QF_UFLRA cases, 500 finite-choice QF_UF cases and 500 finite-choice QF_UFLRA cases. A separate campaign passed 100 OpFuzz mutations of the three regressions and two real QF_UFLRA seeds. There were no wrong answers, crashes, parser/type errors, unsupported results, reference disagreements or timeouts in these gates.

Separate Dolmen replay accepted all 2,011 SAT models from the general and finite-choice QF_UFLRA gates, 68 SAT mutant models, four SAT seed models, and the twelve regression/profile models. The finite-choice QF_UF gate compared answers with Z3 and cvc5; it did not include Dolmen replay. These are bounded samples: the three generated corpora contain 2,992, 42 and 42 distinct input files, respectively, and the mutations contain 80 distinct files.

The qualification summary and run ledger retain exact revisions, binary hashes, commands, seeds, counts, resource limits and job IDs. An initial test attempt failed to locate its fixtures from the CTest working directory; the paths were corrected and all gates rerun on a953edd. That superseded attempt is recorded separately. That qualification closed D-006. The later six-finding qualification follows; publication rights and GitHub handoff remain separate.

Supporting tools and resource controls#

Closed on the qualified solver revision 5c96568. The follow-up qualification and machine-readable report record the fresh eight-route gate, bounded-budget replays, independent ground-model checks, real-seed mutations and release/ASan checks. The run ledger retains superseded attempts and exact commands, hashes and job IDs.

Finding	Repair and regression evidence
A-012: negative `auto` budgets	Exact `auto`/`unlimited` or unsigned decimal parsing; malformed spelling and overflow fail before solving. CLI regressions preserve zero and leading zeros. Parser and CLI regressions; implementation `241a873`.
A-013: incomplete conflict-budget enforcement	Typed `:theory.conflicts` accounting and uniform runtime/callback boundaries across ground, quantified and retained routes; consumption survives retries/fallback and resets per query. Session/component tests cover lazy/online checks, integer conflicts, exact single counting and callback completion. Runtime, session tests and component tests; initial repair `a03fe0d`, callback repairs through `451d0a1`, final fixture `5c96568`. The 800 bounded replay samples supplement the regressions, with one timeout kept incomplete.
B-012: analyzer binding scope	Iterative lexical expansion evaluates parallel right-hand sides in the outer environment and preserves nested shadowing without capture. Malformed and unsupported bindings fail explicitly. Analyzer and scope regressions; implementation `11cd06f`/`d16acb4`. The separate DAG redesign remains deferred.
B-013: composition model-validation selection	Successful SAT rows only, deduplicated by profile/input, `--expect-sat`, exact coverage joins, explicit incomplete results and no validator for an empty selection. Changed SAT-to-UNSAT answers fail even with `--allow-inconclusive`. Composition runner and selection regressions; implementation `11cd06f`/`519b7b5`.
B-014: tuning exit-status handling	Both wrappers check timeout and abnormal exits before answers, apply PAR2 errors and retain output/status. Normal wrong-answer penalties remain. irace, SMAC and mocked-process regressions cover post-answer failures, signals and timeouts; implementation `a194937`.
C-004: numeric probe-name collisions	Locale-independent round-trip thresholds, canonical signed zero and stable nonfinite spellings. Adjacent finite values and locale tests cover descriptions/fingerprints. Probe implementation and identity regressions; implementation `241a873`. Affected fingerprints change; historical records remain unchanged.

These are separate from an external URL that cannot be reached. The external-link report records certificate, access-denial, rate-limit and timeout failures without suppressing them.