fact: Definition setup_checker_step_debug d used_roots (c:certif) := let (nclauses, t, confl) := c in let s := add_roots (S.make nclauses) d used_roots in (s, fst t).
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker