fact: Definition checker_ext d used_roots (c:certif) := let (nclauses, t, confl) := c in Form.check_form t_form && Atom.check_atom t_atom && checker C.is_false (Euf_Checker.add_roots (S.make nclauses) d used_roots) t confl.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker