Skip to main content

check_vacuity

logicaffeine_proof::bmc

Function check_vacuity 

Source 
pub fn check_vacuity(antecedent: &ProofExpr) -> VacuityOutcome
Expand description

Vacuity: can antecedent ever be satisfied? An unsatisfiable antecedent means the property is never actually exercised (a vacuous pass / dead trigger).