fact: Definition checker_b t_form l (b:bool) (c:certif) := let l := if b then Lit.neg l else l in checker t_form l c.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker