fact: Definition _checker_ (s: S.t) (t: _trace_) (confl:clause_id) : bool := let s' := List.fold_left check_step (fst t) s in is_false (S.get s' confl).
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker