Function check_refutation 

pub fn check_refutation(
    num_vars: usize,
    original: &[Vec<Lit>],
    learned: &[Vec<Lit>],
) -> bool

Verify a DRAT/LRAT-style refutation: every learned clause is RUP w.r.t. the database built so far, and the full database is then refuted by unit propagation (the empty clause is RUP). Returns false if any step does not check — so a corrupted or bogus trace is rejected.