fact: Definition add_roots s d used_roots := match used_roots with | Some ur => foldi (fun i s => let c := if (ur.[i]) <? length d then (d.[ur.[i]])::nil else C._true in S.set_clause s i c) 0 (length ur) s | None => foldi (fun i s => S.set_clause s i (d.[i]::nil)) 0 (length d) s end.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker