fact: Definition resolution_checker s t := _checker_ (fun s (st:step) => let (pos, r) := st in S.set_resolve s pos r) s t.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker