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