Integer-arithmetic preservation map

This section-level audit for the LIA chapter was checked on 2026-09-29 against the original QF_LIA development chapter. The old file and HTML anchors remain available in the historical book.

Preserved means that the new destination explains the mechanism or contract. Superseded identifies a claim corrected against the current implementation. Retained history identifies the exact old section preserved in the dated archive. Retaining history does not revalidate an experiment. The assembled site now checks the archive paths and redirects at every build.

Section destinations

Line links identify old sections at the centrally pinned source revision; destination links lead to explanations in the current manual.

Original section	Disposition and exact destination
Introduction and paper basis	Preserved in stage order and sources. Stage numbers remain development chronology, not execution order.
Scope	Preserved in input lowering and limits: constant-divisor extensions are supported; QF_LIRA is not.
Where branching lives	Preserved in ownership, scheduling, explanations and models. Historical check_sat.cpp locations are replaced by the owning functions.
The search	Preserved in branching, including return states and checkpoints. Bounds-only rollback is qualified for the optional SOI path.
Int in the frontend	Preserved in input lowering and core representation. Pass-by-pass policy is preserved in integer preprocessing profiles.
Integer strictness and three bugs	Current rules and polarity examples preserved in integer bounds. Rejected atom-level tightening, naive threshold offsets, wrong auxiliary-variable rounding and their runs remain history at this link. The early delta-free-assignment claim is superseded.
GCD-consistency	Preserved in row divisibility, with scaling, both bound reasons and every-variable guards. Bugs 4/5 and the suspected extended-test formula erratum remain history. The early statement that all row terms are declared integers is superseded by the pivot-aware rule.
Gomory cuts	Preserved in cuts: eligibility, four coefficient cases, derivation, both worked examples, the 3x+5y=7 regression, private-row lifetime and the rejected need for backtrackable cut rows.
Patching	Preserved in patching: basic and nonbasic cases, freedom intervals and feasibility. A fixed variable’s interval is a singleton, correcting the old “empty” wording. Historical motivation and cube comparison remain at the old location.
Two things the obvious implementation gets wrong	Preserved in the patching example, including oscillation avoidance, target window, indexed scoring and counters.
The one LraTableau change	Preserved in ownership, patching, integer helpers and rollback. Development chronology remains history.
Patching: Result	Retained history: sample comparison, model checks, unavailable local Dolmen and limits of its substitute. Current obligations are in the correctness guide.
Patching: Full corpus	Retained history: SLURM 128125, both arms, gains, losses and search-trajectory cost. Current controls/counters are in patching and budgets.
Conflict generalization: mechanism	Preserved and corrected in explanations. Clause containment establishes neither validity nor sufficiency of the collected reasons.
Conflict generalization: measurements	Retained history: sample comparisons, SLURM 127949, whole-corpus churn and the rings regression. The new chapter preserves the tradeoff without presenting the old diagnosis as a fresh measurement.
Node limits	Preserved in budgets, with actual counter semantics and zero-budget behavior.
Known incompleteness	Preserved in the unbounded interval example. The suggestion that a cube test could close an integer-infeasible case is superseded: failure of that feasibility test cannot prove infeasibility.
QF_LIRA overview	Preserved in representation and limits. 3*x <= 5 is corrected to a direct bound, not an auxiliary row.
Each stage with a non-integer variable	Preserved in the individual patch, GCD, cut and branch contracts.
What blocks QF_LIRA	Preserved in limits: subset APIs do not provide typing, coercions, admission or mixed model integration. The historical whitelist is not copied as a current global capability list.
Status of the QF_LIRA claim	Preserved in limits. No end-to-end mixed-input qualification is claimed. The proposed experiment remains a proposal at the old location.
Explicitly out of scope	Current omissions preserved in limits and cuts. Blanket div/mod rejection is superseded by lowering. The cube counts cited from Bromberger are that thesis’s results, not Primo results.
Fuzzing: commands, campaigns and setup	Retained history: smoke recipes, SLURM 129508/129527, partial mutation coverage, non-passing strict replay, corpus staging and tool cost. Obsolete operator exclusions are not copied into the input contract. Maintained workflow extraction is explicit below.
Fuzzing: defects and stage gates	Retained history: nonbasic auxiliary-variable bug, Dolmen grammar handling, failing jobs and replacement gates. Lasting correctness conditions are in GCD and coverage.
Where QF_LIA stands, 2026-08-26	Retained history: revision 16d0d96, SLURM 130136, comparison table and cactus figure. Evidence preserves the exclusion of clean unknown and timeout rows from solved counts.
Real-world evaluation and the fuzzing gap	Failure mechanism and structural seed diversity preserved in coverage. Failed probes, coefficient-width negative result, repair sequence and counts remain history at this link.
Tests	Preserved in regression obligations, with current test paths and extension support. Old stage numbers and blanket division rejection are superseded.

Evidence identities

The original chapter is still the archive location. Relevant entries in the run log include:

• 2026-08-20-qf-lia-real-world-benchmark-evaluation and 2026-08-20-qf-lia-mutation-fuzz-gate-slurm-verification: failures missed by generated-input campaigns and the pivoted-auxiliary-variable repair.

• 2026-08-21-qf-lia-conflict-generalization and 2026-08-21-qf-lia-conflict-generalization-full-corpus: clause-size comparisons, gains and regressions.

• 2026-08-21-qf-lia-patching and 2026-08-21-qf-lia-patching-verification: development and qualification records.

• 2026-09-03-qf-uflia-indexed-patching-local: the later affected-column scoring check. Local execution is historical provenance, not a current instruction to run solver batches locally.

Destinations outside the integer algorithm chapter

The preprocessing chapter now covers integer profile selection, restricted optional passes, mandatory translation, and model conversions from the old frontend policy.

Preserved in fuzzing: seed selection/staging, mutation restrictions, visited-seed limits, and outcome classification. Independent validation records Dolmen grammar modes. Historical machine-specific counts remain in their dated records.

This audit covers the original LIA development chapter. It does not certify the separate integer-division literature note, profiling report, all integer open leads or the whole corpus. Their sections are accounted for in the complete inventory, with current literature and research mappings. The archive routes are installed; reader acceptance remains pending.