Skip to main content

prove_unsat

logicaffeine_proof::sat

Function prove_unsat 

Source 
pub fn prove_unsat(e: &ProofExpr) -> UnsatOutcome
Expand description

core for equivalence, bounded model checking, k-induction, and vacuity.