        bdd::SatResult::Error => panic!("SAT check error"),
    }
}

pub fn do_bddsat(f: &Formula) {
    let r = bddsat(f);
    let sr = cnf::write_sat_result(&r, &mut io::stdout());
    sr.unwrap_or_else(|e| println!("{}", e));
    let vr = cnf::write_sat_valid(f, &r, &mut io::stdout());
    vr.unwrap_or_else(|e| println!("{}", e));