Move QF_UFLRA to the general component driver

Status: Open lead. Owner: unassigned.

Consolidate the dedicated Real route onto the existing general component driver. Integration planning and migration remain open. The general driver is already implemented and used by QF_UFLIA and quantified UF; this proposal concerns bringing QF_UFLRA onto that driver.

Implemented baseline

The combination chapter describes both routes. solve_component_recipe owns the general SAT loop and component lifecycle, configured by CombinationRecipe. QF_UFLRA retains its dedicated engine. The completed component migration record preserves the earlier scope and qualification; that work deliberately left the Real route in place.

Scope and first review

Map the Real engine’s responsibilities to the existing component contracts: explained equality exchange, internal model reconciliation, scratch mutation, explanation lifetimes, model construction, and exact fallback. Preserve typed inconclusive results, shared assignment ownership, and current options. Record any contract gaps before choosing an implementation sequence.

Use the dedicated route as the behavioral and performance baseline. Reuse the chapter’s invariant-to-test map, then run fresh correctness gates, independent model validation, and paired evaluations before switching production dispatch. The old qualification record does not qualify a future migration.

This is an architectural consolidation. The further model-based transition investigation and care-guided combination investigation have separate algorithmic and correctness obligations.