Function check_spec_vacuity 

pub fn check_spec_vacuity(
    spec_source: &str,
    bound: u32,
) -> Result<VacuityReport, HwError>

Vacuity check (Z3-free, certified): does the property’s trigger ever fire? An unsatisfiable antecedent means the property passes vacuously — a dead trigger that usually signals a malformed spec. Reuses logicaffeine_proof::bmc::check_vacuity.