Function crush 

pub fn crush(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    budget: usize,
) -> Option<bool>

The unified crush. Compose every lever into one decision procedure: carve the autark sections (pure literals), split into independent components, and decide each by the cut-enabled symmetry-aware search — a component refuted by a certified cut at the root closes in one node, the rest fall to bounded branch-and-cut. The formula is UNSAT iff any component is, SAT iff all are. Returns None only when a component blows past the budget — the genuinely hard residue, honestly surfaced rather than hidden.