N-component combination migration

Status: migration implementation at 2413397 and its five-logic qualification are complete. The subsequent order-preserving coordinator optimization at b883d6f has separate QF_UFLIA qualification below. All original migration per-logic performance limits pass, every successful candidate SAT row has an independently validated model, and all prescribed lost-solve follow-ups are finished. The production QF_UFLIA route uses the collection driver, dispatcher and fragment assembler. Generated and real-seed campaigns found no correctness failures, with explicitly inconclusive resource rows retained below. The sample, watchlist and full 659-input paired QF_UFLIA gates pass, including independent replay of every candidate SAT model. Known reference timeouts, baseline-only UNSAT evidence and resource-inconclusive fuzz/follow-up rows remain explicit below. The frozen external binary remains the baseline; qualification is not a claim of a uniform family speedup.

Scope and frozen boundary

The accepted objective is an extensible N-component combination architecture, including production QF_UFLIA dispatch, incremental execution and model export. Independent test components demonstrate three and four participants without adding a user-visible theory. The dedicated QF_UFLRA route, its experimental generic route, legacy callbacks and scheduling remain unchanged. New adapters may use unchanged Primo kernels; no other solver implementation is a source.

The source baseline is 75d5177 (solver sources identical to 287b743). The retained Release/CaDiCaL 3.0.0 baseline binary has SHA256 5a671d47882f555f3522c92b7b6c05a76c3bbdfde6ec2cb714b69e76c519b3f7. Its full-corpus results are recorded in run-log.json; they are historical comparison evidence, not validation of the migration.

Sources and proof obligations

Read for this migration:

• de Moura and Bjorner, Model-based Theory Combination, ENTCS 198(2), 2008, pp. 37–49, DOI https://doi.org/10.1016/j.entcs.2008.04.079; [10], Sections 2.1, 4, 5.1 and 5.2.

• Bruttomesso, Cimatti, Franzen, Griggio and Sebastiani, Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis, LPAR 2006, LNCS 4246, pp. 527–541, author manuscript, Sections 2 and 3, Figure 4. Complete arrangements do not require convexity or complete equality deduction. We do not claim the paper’s NO-emulation branching bound or its specific last-UIP/negative-first strategy.

Model coincidences create reversible SAT decisions, never entailed equalities. Only explained consequences become clauses. A component’s complete projection must satisfy every assigned interface relation in its scope. After mutation, check that obligation again and recompute comparison edges, including edges not mentioned in the mutation request. Bounded model guidance retains the complete-arrangement fallback. This is a transition subset, not Appendix A’s full DPLL(T^M) implementation; this migration adds no new simplex algorithm.

The following many-sorted normalization is an original implementation design. It applies the arrangement construction to each connected sharing group. Stable infiniteness means simultaneously infinite domains for the declared shared sorts, not separate models witnessing infiniteness one sort at a time. Bool and other finite shared domains are not admitted by this protocol. Disjoint interpreted signatures and explicit atom ownership are preconditions.

Representation and operations

Implemented production architecture:

• theory::TheoryComponent: solve-scoped component lifecycle and immutable descriptor; no SAT backend or SMT-LIB AST. It owns preparation, incremental state, explanations and model contributions. Terms are referenced by stable TermId, never arena references retained across construction.

• smt::TheoryCombinationPlan: validated descriptor copies, atom-owner routes, and normalized per-sort scopes. Unowned/ambiguous atoms and unsupported signature or sort combinations are Unsupported, not UNSAT.

• smt::ComponentModelCoordinator and smt::ComponentDispatcher: component collections and recipe priorities; no EUF/LIA name tests. Online checking remains EUF-first and model guidance arithmetic-first through those priorities. Assignment deltas use precomputed routes, not a component scan per literal.

• smt::solve_component_recipe owns Boolean abstraction, equality bridge clausification, assumptions and failed-core blocking, component preparation, typed stop handling and complete-arrangement restart. CombinationRecipe supplies component factories and independent online/model priority orders. Normal disagreement creates one equality choice per round, preserving the baseline policy; only explicit mutation candidate lists can batch choices.

• theory::ComponentModelFragment declares authoritative typed values, retained facts and symbol contributions. Local domain identities are namespaced by component. validate_component_fragment checks the exact accepted token, native authoritative coverage, uninterpreted shared-variable coverage, symbol ownership and agreement with the accepted partition or complete arrangement. assemble_component_model identifies local domain labels using shared terms before constructing evaluated function tuples. Identification may not collapse two distinct values from one component. Conflicting native values, facts or rows are errors, never last-write-wins. The resulting core::Model owns an immutable interpretation. Conversion steps replay in reverse execution order, and final assertions are evaluated; the session separately checks original assertions with --check-model.

Production UfliaEufComponent and UfliaLiaComponent currently live beside their preparation helpers in solver_engines.cpp. They expose no SAT backend or private model state through TheoryComponent. ComponentAssignmentView owns atom-registration metadata and reads the shared assignment owner; it has no mutable truth values, literal trail, or decision boundaries. Callbacks route deltas without rescanning the full atom set. Offline recipes populate one completed-model snapshot through the same view API. Interface growth detaches the dispatcher before extending preparation and rebuilding live callbacks. LIA exports exact values from its private integer-completed model; EUF exports retained facts, not arbitrary numeric anchors. Arithmetic remains first for full-model reconciliation and EUF first for online checking.

Two algorithmic duplications remain after the shared-assignment migration: ComponentLraExecution ports Primo’s existing online arithmetic execution with phase publication replacing its backend reference. Both arithmetic execution classes now read the shared assignment view and retain their own tableau undo. FragmentModelBuilder extends Primo’s existing typed reconstruction algorithm behind the fragment boundary; the old typed builder remains unchanged for QF_UFLRA and the other routes. These are not new simplex or reconstruction algorithms, nor copies from another solver. Moving engine-local preparation helpers into theory-owned files can follow without changing the public protocol. The driver accepts purified atoms; admission rejects escaped mixed arithmetic applications rather than assigning an ambiguous owner. The QF_UFLIA front-end purification transformation itself retains the existing semantics.

The new coordinator validates projection epochs, component identity and exact scope coverage before comparing partitions. A descriptor change after planning is rejected. Care capability gates care queries; care pairs rank decisions, not acceptance. The dispatcher retains per-component assignment buffers and an indexed SAT-variable route. Partial checks visit only dirty components in recipe order; reasons for surviving root propagations survive unrelated backtracking. Typed cancellation/resource/unsupported results are saved for the owning solve loop, never converted to an empty clause.

tests/unit/component_combination_tests.cpp checks 432 three/four-component cycle/order/policy combinations using CaDiCaL against exhaustive partition enumeration. Additional tests cover two-sort nonparticipants, disconnected scopes, capability rejection, nonconvex disjunctions, malformed/stale models, mutation side effects, fixed decisions and incremental explanation lifetime. Another 432 cycle/policy/online combinations use solve_component_recipe end-to-end, including SAT assumptions, sparse growth, callbacks and fragment model assembly. model_tests.cpp deliberately supplies stale exports, missing shared bindings, partition-inconsistent values, conflicting numeric bindings, fractional Int values and duplicate function rows. It verifies component-local domain remapping and immutable table ownership. These tests are correctness evidence, not performance or corpus-validation evidence.

Foundation verification (2026-09-08): make check passed (29 CTest targets and 107 Python tests); make asan-test passed all 29 targets; make docs and make lint passed. Focused clang-tidy on the four new .cpp files passed without warnings. The whole-tree tidy attempt reached the local 120-second limit; its completion belongs to the SLURM verification gate. The advisory include scan was rerun on the final new files after a concurrent-edit snapshot proved unusable. No production fuzz/performance claim follows from these tests.

Connected-candidate verification: all 29 CTest targets and 111 Python tests pass; lint and documentation builds pass. A byte comparison against 75d5177 confirms the QF_UFLRA engine tail and legacy callback region are unchanged (the removed helper belonged only to QF_UFLIA). The first ASan pass caught a stack-use-after-return in the new EUF adapter: OnlineEufPropagator borrowed options created inside reset(). Options now belong to the adapter, precede the callback in destruction order, and the callback is destroyed before configuration/preparation changes. The existing evaluated-argument regression reproduced this under ASan; after the fix make asan-test passes all 29 targets. Focused static review of the new driver, assembler, dispatcher, coordinator and their tests reports no owned code warning. Subsequent whole-tree review and generated-campaign results are recorded below and in the run log; performance was still pending at that stage. A passing ordinary build was not used as lifetime evidence.

For each sort, build the component graph whose edges mean occurrence of the same interface variable. In each connected group, form the union of variables occurring in at least two original components. Register that whole union with each group participant, including unconstrained vocabulary extensions. Projections must cover that scope exactly. A component outside the group is never compared or mutated for it. Pair keys contain sort and canonical term IDs.

Example: A has {x,y}, B {y,z}, C {x,z}. All three receive {x,y,z}; otherwise independent pairwise agreements could miss x=y, y=z, x!=z. Disconnected groups and different sorts keep distinct scopes. EUF+LIA keeps exactly its old shared-Int intersection, avoiding an interface-size regression. Plan construction uses indexed occurrence lists and connected components; projection storage is linear in normalized scope size. Complete fallback may enumerate quadratically many same-scope pairs, as in the baseline. Model-guided comparison should use class spanning edges rather than an unconditional pair cross-product. No live row insertion into a trailed tableau is introduced: interface growth uses the established callback rebuild boundary.

Acceptance checklist

Linear ordinary-decision selection (2026-09-09)

The Certora profile recorded in 2026-09-09-certora-migration-diagnosis found 30.6 million ordered-set insertion-position searches and 15.3 million tree lookups in one check. The following local design removes that overhead; it does not restore the pre-migration heuristic or change the theory algorithm.

• Existing order: after mutation, sort normalized (sort, lhs, rhs) keys, place care pairs first, then choose the first disagreeing pair. One ordinary equality is requested per SAT round. Explicit mutation candidates are separate.

• Selection invariant: retain only the minimum disagreeing care key while validating every supplied care pair. If one exists, no non-care edge can win. Otherwise scan the post-mutation equal-class spanning edges and retain the minimum disagreeing key. Duplicate/reversed care pairs do not affect the minimum.

• Proof obligation: dropping agreeing pairs and duplicate keys cannot change the first disagreement in the old care-first lexicographic order. If no care pair disagrees, care membership cannot affect the remaining choice. Spanning edges still establish partition agreement; never compare nonparticipants.

• Ownership: selection keeps one value-owned key, not borrowed term storage. Projection indices are solve-round local; no cached conclusion survives a mutation, assignment epoch or backtrack. Validate all care-pair scopes even after finding a candidate, so malformed later entries cannot be hidden.

• Cost: ordinary selection uses linear scans in supplied care pairs and, only when needed, spanning edges, with participant comparisons per pair and constant additional candidate storage. It allocates no ordered candidate sets. Existing projection indices, care-vector ownership, mutation machinery and complete-arrangement fallback are unchanged.

• Tests/evidence: lock care priority, lexicographic tie-breaking, duplicate and reversed keys, late invalid care entries, no-care fallback and agreement; keep the three/four-component oracle. Collection-owned ComponentModelStatistics extends the legacy statistics without changing the frozen coordinator. The counters :combination.model.care-pair-agreements and :combination.model.spanning-pair-checks count visits, including duplicates. Compare real search counters as well as timings, and independently replay every successful candidate SAT benchmark row.

Implementation passes 29 CTest tests, 128 Python tests, all 29 ASan tests, lint and documentation build. The added order oracle checks 2,325 configurations across two, three and four components; the large agreeing-care test visits 50,000 entries without constructing an ordered candidate set. The implementation at b883d6f is accepted against the frozen post-migration 2413397 baseline, not against the older equality-choice heuristic. Fresh SLURM evidence is recorded in 2026-09-09-linear-component-selection in run-log.json:

• The 25-input quick gate (previous sample and watchlist plus Certora 47) preserves 24/25 solves in both rounds and reduces common-solved time by 19.91%. Its 26 candidate SAT models all pass direct Dolmen validation. The committed manifest is benchmarks/component-linear-quick-25.txt.

• The full 659-input, 60-second gate preserves 575 solves and 84 timeouts in each round for both binaries: no gains, losses, wrong answers, disagreements, errors or unsupported rows. Across both rounds, common-solved time falls from 2,566.665184 to 2,495.783937 seconds (2.76%); PAR2 falls from 22,726.665184 to 22,655.783937 seconds (0.31%). Common-time family reductions are Certora 10.17%, TwoSquares 0.93%, mathsat 1.36% and wisas 2.94%. Individual runs can still vary; the run log retains the two round-one mathsat regressions above 10%.

• All 425,500 existing non-timing counter comparisons match across the 1,150 common-solved executions. This corroborates the selection-order proof and unit oracle; aggregate counters alone are not a complete equality-by-equality trace. Both full rounds’ 810 SAT models pass separate direct Dolmen replay, with complete coverage and unchanged hashes. Every decisive answer agrees with hash-matched recorded reference results; no corpus reference solver was rerun.

• Certora 47 falls from 35.433517/36.050354 to 26.638193/26.514294 seconds in the full paired run, with unchanged search counters. Five separate instrumented runs retain those counters and no longer show the former ordered tuple-set insertion/lookup hotspot. EUF care-pair generation/sorting and arithmetic checking remain costs; this does not claim that all combination work is free.

• A fresh generated gate passes 4,000 comparisons (3,000 default, 1,000 online disabled) and all 2,032 SAT-model checks. Supplemental real-seed mutations retain 1,435 inputs: 1,398 answer passes, 951 Dolmen passes, 447 UNSAT model rows and 37 solver timeouts. Original seeds add 14 answer passes and two timeouts. These mutation jobs retain their failed/resource-incomplete status, not an all-pass label; classification finds no crash, invalid model, bad input or answer disagreement. The generated gate is fully green.

• Whole-tree clang-tidy and advisory include scans cover all 105 non-generated C++ files. No new blocking findings: the existing tactic.cpp shared-pointer analyzer warning and transitive-provider/self-include advisories remain explicit in the run log. No QF_UFLRA source path changed, and this follow-up does not claim a fresh rerun of the earlier five-logic qualification.

Timing jobs are 140614 (quick) and 140620 (full); independent full-model replay jobs are 140696/140697. Raw evidence and retained binaries are under results/n-way-linear-b883d6f. The historical migration results below remain evidence for 2413397 only.

Adding another component

This is the implemented extension path, not a claim that arbitrary SMT theories already satisfy the combination preconditions. A new kernel still needs its own paper-grounded design, soundness argument and fragment tests.

1. Implement theory::TheoryComponent with a solve-owned lifetime. Keep kernel state private. Publish an immutable ComponentDescriptor with a unique ID, supported fragment, disjoint interpreted families and owned function symbols. Declare convexity and joint stable infiniteness accurately; complete equality propagation is a separate capability, not a consequence of writing “convex”.

2. Define exact owns_atom and interface_variables behavior on purified terms. Every original or generated atom must have exactly one owner. Shared variables must be free constants. Support registration of unconstrained scope extensions when the sharing graph requires them; do not infer the scope from only the component’s original atoms. Finite shared domains and overlapping interpreted signatures remain outside this protocol.

3. Implement registration, reset, level changes and assignment deltas. With an online recipe, declare and implement incremental support. Explanations must remain valid after unrelated backtracking; resources and unsupported cases return typed stops. encode_equality returns an equivalent Boolean formula; the SMT driver, not the kernel, creates SAT clauses and owns the backend.

4. Provide complete, fresh model projections when claiming that capability. Missing projection support selects complete arrangements. Mutations must preserve assigned relations and advance model revision. To produce a final model, declare export support and return an owned fragment for the exact accepted token. Cover shared bindings, namespace domain identities locally, and export only owned symbol interpretations. A shared sort may have at most one authoritative value owner in each connected group.

5. Add a factory to smt::CombinationRecipe. Its Boolean argument selects model-guided versus complete mode, including fallback reconstruction. Factory order sets reconciliation priority; online_order must be a permutation of every component index when online execution is enabled. Set the bounded decision budget deliberately. No component-count or theory-name branch is needed in the collection driver, and no QF_UFLRA route change is required.

6. Extend the independent partition-oracle tests in tests/unit/component_combination_tests.cpp, including reordered three/four participant recipes, disconnected sorts, sparse growth and complete fallback. Exercise solve_component_recipe with model production, not just the coordinator. Add negative fragment/lifetime/explanation tests, exact-profile fuzzing, independent model replay and paired performance preservation before admitting the new production recipe.

Queued lemmas

Added for quantifier instantiation (M3 in Quantifiers: parsing and term representation). No theory kernel changed; only the component protocol and the online driver grew.

• theory::TheoryCheckStatus::LemmasPending. A component has queued closed Boolean formulas, possibly over atoms that do not exist yet, each a valid consequence of the assertions.

• TheoryComponent::take_lemmas(limit). Hands over up to limit of them. The default returns none.

• ComponentCapabilities::check_on_full_model. The dispatcher consults such a component only at cb_check_found_model, and there on every complete assignment, even when none of its atoms changed, so a complete assignment is never accepted without it. Mid-search checks skip it and leave it dirty.

  Consulting it earlier broke quantified UF. Quantified assertions are root units, so the quantifier component answered LemmasPending at the first check of every round. That stop muted the ground components before the search reached a conflict that needed decisions, and SAT accepted a propositional model. Easy unsat problems went unknown whenever new instances kept coming (sledgehammer/FFT/uf.860560, grasshopper find_last_check_heap_access_14_2).

• ComponentDispatcher::lemmas_pending(). The dispatcher records the stop there, not as a failure. It then makes no further checks, decisions or propagations for that solve.

• Draining in solve_component_recipe. When SAT returns a model with a stop pending, the driver:

  1. drains up to CombinationRecipe::lemma_batch lemmas from the owning component;

  2. disconnects the previous dispatcher, passes the lemmas through CombinationRecipe::prepare_lemmas and clausifies the result, including all lowering definitions;

  3. calls install_atoms(), which first completes Boolean-domain preparation, then registers every new atom with its owner and rebuilds the dispatcher;

  4. solves again.

  An UNSAT result with a stop pending is still UNSAT, since lemmas only strengthen the formula. Without prepare_lemmas the stop is Unsupported. The same installation checkpoint prepares generated interface encodings. Initial planning also runs preparation before taking the registry snapshot; the hook must be idempotent. See Boolean Arguments in EUF for the generated-term ownership and lifetime contract.

• Counters. :combination.lemmas.batches and :combination.lemmas.formulas appear only when lemmas are drained, so existing recipes’ statistics are unchanged.

• Outside the online dispatcher. A LemmasPending result from a full-model check is Unsupported: the model-based coordinators cannot drain queues.

tests/unit/component_combination_tests.cpp covers:

• a lemma over a new equality atom that is later refuted;

• a new atom that must reach its owner at the growth boundary;

• a component consulted only through check_on_full_model, and the same component without the capability (Unsupported at reconciliation);

• a missing preparation hook;

• a queue drained one lemma per boundary.

Migration gates

• Validated contracts, ownership and capability planning.

• Participation normalization and three/four-component SAT integration tests.

• Freshness, mutation, fixed-decision and typed failure regression tests.

• Collection dispatcher and production incremental EUF/LIA adapters.

• Generic model export/composition, including corrupted-model rejection.

• Full production QF_UFLIA migration; frozen QF_UFLRA source preserved.

• Validator resource classification and explicit Dolmen memory budgets.

• Check, ASan, lint, docs, whole-tree static/code and efficiency review.

• Exact-candidate generated and real-seed mutation coverage for all selected profiles; at least 3,000 default generated cases. Resource-only outcomes are triaged below, not counted as passes or an unconditional green campaign.

• Independent Dolmen replay of every candidate real-corpus SAT row, separate from speed measurement; resource failures are unvalidated, not invalid models.

• Paired baseline/candidate SLURM sample, watchlist, full 659 QF_UFLIA and five-logic preservation suite, 60-second full-corpus cap. Alternate run order on the same node, then repeat with reversed order. Each logic must stay within 1% for PAR2 and common-solved runtime; any lost solve gets three paired reruns and a loss in at least two blocks acceptance. Report families and all outcomes.

• Reuse recorded reference answers/timings and preserve binary/corpus/build/option provenance. Known reference timeouts remain inconclusive; no reference sweep was rerun. Two QF_LIA UNSAT inputs have only frozen/historical baseline support, not declared or independently checked status.

• Coherent verified commits and canonical run-log entries for every gate.

No new permanent CLI profile is planned. Default promotion requires all gates; the frozen external baseline is the A/B control. Operational details belong in the existing testing, benchmarking and model-validation skills, not AGENTS.md.

slurm_component_migration_compare.sbatch takes explicit baseline/candidate binaries and expected revisions, runs both on the same allocated node, reverses their order for a second paired round, and records hashed provenance through benchmark_model_replay.py. An optional ordered manifest selects the sample or watchlist before sharding. It launches no reference solver. Each candidate round’s SAT rows are subsequently replayed by a separate validation job. Both scripts explicitly require one node and one task: they launch one serial Python harness, not a distributed program. Select eligible timing nodes through exclusions or constraints; without the explicit node-count limit, a multi-node --nodelist can reserve every listed node. Inspect the allocated node/task counts immediately after submission. The cluster’s allocation-only check with --nodes=1 --ntasks=1 and a two-node list selects just one node; it does not reject that combination of arguments.

slurm_component_loss_rerun.sbatch performs exactly three baseline/candidate pairs on an explicit lost-solve manifest, alternating order within one allocation. Use one input per shard with its default ten-minute allocation and 60-second solver budget. It forwards the same profile options and records the same hashed provenance as the full comparison; no reference solver is launched. A candidate loss in at least two of the three pairs blocks acceptance. These focused repetitions do not replace the full-corpus aggregate timing thresholds. Any SAT answers produced by the reruns still require separate model validation. summarize_component_pairs.py --loss-reruns --expected-count N ROOT validates all three pairs’ provenance and reports per-input loss counts and the two-loss threshold separately from the original timing verdict. Process errors, wrong answers or unsupported output cannot be accepted as ordinary cutoff variation.

On this cluster, some aftercorr replay tasks remain dependency-pending even after their matching timing task reports COMPLETED 0:0. slurm_release_completed_replays.py is an explicit, dry-run-first workaround: it selects only pending replay indices with successful source accounting and validates all four timing artifacts, source run IDs, binary/input hashes, options, budgets and row coverage before permitting --release. It clears only those verified tasks’ dependencies; it submits no job, repeats no timing, and leaves still-running source indices untouched. Replay itself still performs its independent input/binary checks. Record each release in the campaign log.

slurm_component_migration_fuzz.sbatch covers the full 16-profile cross-product of preprocessing auto/off/basic/strong, model guidance on/off and online mode on/off. Four shards give the default profile 3,000 generated mixed inputs and each other profile 1,000 (18,000 total). One shard per profile first checks all tracked regression and QF_UFLIA smoke seeds against the reference, including exit-status and declared-answer checks. SAT outputs require direct Dolmen validation. slurm_component_migration_mutation.sbatch uses the same profiles and deterministic smallest-per-family real seeds; oversized seeds are errors, not silently omitted families. Its retained mutants undergo separate model validation with the exact same solver options. The standalone TypeFuzz gate explicitly selects the existing linear-integer configuration, but operator selection alone is insufficient: generative TypeFuzz can replace a literal coefficient inside an existing multiplication with a nonconstant expression. Both attempts are retained as rejected harness evidence, not valid-input campaign coverage. The qualification matrix therefore uses the existing seeded OpFuzz profile (model_linear_ops.txt), which changes operators without generating new operands. The existing typed-model mutation gate checks original seeds and every retained mutant with status-aware reference comparison and independent model validation. Default mutation iterations are 100 per family seed, bounded by the campaign wall time. No candidate rejection is ignored to make a gate pass; out-of-fragment attempts remain in the run log. The original-seed precheck has a separate 60-second budget; short mutated-input checks retain a five-second budget. In this qualification matrix, classify_mutation_resources.py permits collection to continue after explicitly classified timeout/unknown/resource rows. It rejects crashes, disagreements, bad inputs, invalid models, changed answers and missing evidence. The original nonzero stage status still fails the final gate; continued collection is not a pass. All seeds remain included. Ordinary typed-model gate callers retain fail-fast behavior unless they explicitly request resource-only collection. Mutant answer comparison ignores inherited seed status metadata, which need not survive an operator mutation, but still compares the two solver answers and process statuses. Original-seed status checks remain enabled.

Whole-source clang-tidy and the advisory include scan completed on SLURM (105 non-generated C++ files each). The include review removed three unused headers from the migrated engine and replaced the indirect exception-type dependency with its owning plan header. The unchanged Goal shared-pointer constructor has one analyzer leak warning: manual ownership review and the ASan leak checks do not support the warning; no suppression or unrelated source change was added.

summarize_component_pairs.py checks completed shard provenance, matching input hashes/options/timeouts, stable binary identities, both paired rounds and node records before reporting timing ratios. It reports family summaries and lost solves separately. Its timing result does not certify models or replace the recorded-reference answer join. join_recorded_reference_answers.py performs that join without running any solver. It requires complete recorded shards and matching input hashes, checks all decisive recorded answers for disagreement, and reports absent reference answers separately. Incomplete historical shards are not reused as complete evidence. Candidate unsolved rows remain unsolved, not verified answers.

The paired sample and watchlist pass their aggregate timing gates, but wisas is slower in both. Its SAT decisions/propagations and combination rounds match the baseline; reconciliation overhead is a profiling target. The larger growth timer alone is not comparable: the new timer also encloses callback rebuilding, which was outside the old growth timer. slurm_component_profile.sbatch builds a separate -pg binary and collects repeated gprof samples without changing either retained timing binary. Instrumented times are diagnostic, not headline performance evidence. No new algorithm is inferred from the timers alone.

Qualification evidence through the full QF_UFLIA stage

The retained 2413397 candidate passed 17,996 of 18,000 generated answer checks; three node-limit unknowns and one timeout remain inconclusive. The default profile passed all 3,000 cases. All 9,134 generated SAT models passed Dolmen, and all 96 tracked regression/profile checks passed. Real-seed operator mutation covers all four families under all 16 option profiles: 2,817 retained mutants yielded 2,453 decisive answer agreements and 364 resource outcomes. Separate model checks yielded 1,514 direct Dolmen passes, 941 UNSAT rows and 362 timeouts. Answer and replay counts differ because two initially incomplete answers became decisive on replay. None of these resource rows is a pass; the collection harness retains a nonzero final status. There were no wrong answers, invalid models, crashes, parser/type errors or reference disagreements.

The full 659-input QF_UFLIA comparison used two same-node, reversed-order baseline/candidate rounds with a 60-second cap. The baseline solved 571 inputs in each round; the candidate solved 574 and 575. There were no lost solves, errors, unsupported results or answer disagreements. Combined PAR2 decreased from 23,309.092340 to 22,808.494721 seconds (2.15%); common-solved runtime decreased from 2,189.092340 to 2,139.664572 seconds (2.26%). All 810 candidate SAT replay rows passed Dolmen directly with an 8G checker budget; all 64 replay shards have complete coverage and unchanged binary/input hashes. Every decisive candidate answer agrees with a hash-matched recorded reference answer. No reference solver was rerun for these comparisons.

This is not a uniform family speedup. Certora gained two solves in both rounds, but its common-solved runtime increased 22.59% (72.301020 to 88.635538 seconds across both rounds). TwoSquares and mathsat common runtime decreased 0.66% and 2.11%; wisas decreased 8.16% over the full family despite the small-probe regression. The extra fourth gain in the second round is near-cutoff variation, not evidence of four robust additional solves. Candidate-only gprof identified routing and pair ordering as follow-up targets at 2413397; no speculative optimization was folded into that migration result. The separately qualified b883d6f linear-selection change above subsequently removes the measured ordered-set overhead without changing the post-migration choice order.

The preservation suite covers QF_UF (7,503), QF_LIA (13,306), QF_LRA (1,753) and QF_UFLRA (1,284) with the same frozen binaries and two paired rounds. The completed 659-input run is reused as the QF_UFLIA leg. Model replay runs on a separate node only after its corresponding timing shard completes. Recorded reference results are reused by content hash. Full acceptance requires each logic’s 1% PAR2/common-runtime limits, any required three-pair lost-solve reruns, and validation of every candidate SAT row; all are now completed with the evidence limitations described below. Exact submissions, artifacts and resource classifications are in run-log.json.

QF_UFLRA preservation is now complete for timing and models: both binaries solve the same 1,270/1,284 inputs in each round (759 SAT, 511 UNSAT, 14 timeouts), with no lost or gained solves. Combined PAR2 increases 0.22% and common-solved runtime 0.73%, within the 1% limits. All 1,518 candidate SAT replay rows pass Dolmen; all 128 coverage files are complete with unchanged hashes. Family common-runtime changes are FFT +0.46%, cpachecker-bmc -0.03%, cpachecker-induction +0.78% and mathsat +0.28%.

Each QF_UFLRA round has 1,265 decisive recorded-reference agreements and five cases where both references previously timed out at 60 seconds. Those five match the frozen Primo baseline and the input’s declared status; two SAT answers additionally have validated models. The three UNSAT answers remain without decisive reference corroboration. The join reports these as inconclusive reference evidence, not disagreements or missing artifacts; no redundant reference sweep is launched to replace known timeout records.

QF_UF preservation also passes after the prescribed lost-solve follow-up. The candidate solves 7,495/7,503 inputs in each round; the baseline solves 7,494 and 7,496. Combined PAR2 increases 0.42% and common-solved runtime 0.48%, within the 1% limits. All 6,284 candidate SAT replays pass Dolmen, with 256 complete coverage records and unchanged hashes. PEQ and SEQ common runtimes increase about 4.5%; this is not a uniform family speedup. One gained QG solve in round zero and one lost PEQ solve in round one remain recorded, not erased as noise. The lost PEQ case solves UNSAT on both binaries in all three focused pairs, matching recorded Z3, so the two-of-three repeated-loss threshold is not met. Its focused runtime ratio is 1.0109; the preservation limit applies to the full-corpus aggregate, while the follow-up tests repeated loss of a solve. Ten other UNSAT inputs have only known reference timeouts, agree with the frozen Primo baseline and declared status, and remain explicitly without decisive reference corroboration. Exact files and both rounds’ family results are retained in the run log and artifacts.

QF_LRA preservation meets the same gates. Across both rounds the baseline solves 3,076/3,506 executions and the candidate 3,075; combined PAR2 increases 0.112% and common-solved runtime 0.089%. All 1,864 candidate SAT rows pass Dolmen, with 128 complete coverage records and unchanged hashes. Four original lost solves and three gains remain in the raw comparison. Exactly three paired follow-ups per lost input find one loss each for Labyrinth and Canberra, none for Gulwani, and both binaries timing out in all three Collatz pairs. Thus no input reaches the two-of-three differential-loss threshold; the Collatz follow-up is resource-inconclusive, not a reproduced solve. Both SAT follow-up models pass Dolmen. DTP-Scheduling and sc common runtime increase 1.87% and 1.30%, respectively, despite the small aggregate change.

The QF_LRA rounds have 1,412 and 1,415 decisive recorded-reference agreements. Both references previously timed out on another 121 and 127 candidate solves: 74/75 SAT models are independently validated, while 47/52 UNSAT answers agree with declared status but lack decisive reference corroboration. Two round-zero UNSAT gains also lack a decisive frozen-baseline answer. These limitations remain explicit; fetching existing cvc5 artifacts to complete the join did not rerun either reference solver.

QF_LIA completes the preservation gate. The baseline solves 9,694 and 9,710 inputs; the candidate solves 9,702 and 9,715. Combined PAR2 decreases from 941,603.044333 to 940,437.614321 seconds (0.124%); common-solved runtime decreases from 75,944.682412 to 75,574.525688 seconds (0.487%). The raw comparison retains 25 gained and 12 lost executions. Every lost input has exactly three paired follow-ups: two inputs lose once each, none twice. Many follow-up pairs time out on both binaries and remain resource-inconclusive, not evidence of recovered solves. All 12,929 successful candidate SAT rows pass Dolmen, with 1,024 complete coverage records and unchanged hashes; all 11 successful SAT follow-up rows also pass. The baseline/candidate totals retain 1,503/1,501 unknowns and 5,705/5,694 timeouts as unsolved outcomes.

QF_LIA family common runtimes increase 1.22% for 2019-ezsmt, 1.43% for arctic-matrix and 1.76% for miplib2003; nec-smt decreases 0.80% and gains 11 solved executions. The per-logic aggregate limit is not a per-family guarantee. Recorded Z3 agrees with 9,507/9,516 decisive answers; another 195/199 have known reference timeouts. Cancelled, incomplete cvc5 shards are excluded. The 69/70 SAT gaps have independently validated models. Of the 126/129 UNSAT gaps, 124/127 match declared status. The remaining two inputs, 20220307-SMPT/RwMutex-PT-r0010w2000/RC-04.smt2 and 2019-cmodelsdiff/wireRouting/wire.12.x.12.b.5.a.20_unsat.data.smt2, have no declared status and agree with historical and both frozen-baseline runs only. That agreement is explicitly not independent UNSAT validation.

Final preservation summary

Changes below compare the frozen candidate with the frozen baseline across both same-node, reversed-order rounds. A positive timing change is slower. All per-logic timing changes are below the agreed 1% regression limit.

Logic	Solved executions, baseline → candidate	PAR2 change	Common-runtime change	Candidate SAT models validated
QF_UF	14,990 → 14,990	+0.42%	+0.48%	6,284
QF_LIA	19,404 → 19,417	-0.12%	-0.49%	12,929
QF_LRA	3,076 → 3,075	+0.11%	+0.09%	1,864
QF_UFLRA	2,540 → 2,540	+0.22%	+0.73%	1,518
QF_UFLIA	1,142 → 1,149	-2.15%	-2.26%	810

All 23,405 successful candidate SAT rows passed direct Dolmen validation, separate from timing, with 1,600 complete coverage records. No wrong answer, error, unsupported result or decisive paired disagreement was found in this suite. Timeout/unknown results, recorded-reference limitations and family regressions remain part of the result. All jobs are finished; exact submissions, binary hashes, family metrics and follow-up classifications are in the 2026-09-08-n-component-preservation-four-logics run-log entry, alongside the full-659 qualification entry. Artifacts are under results/n-way-2413397/preservation-v2, full659 and loss-reruns on the recorded SLURM workspace, with collected summaries locally.