fact: Definition ignore_true_step (st:step) := match st with | CTrue _ | @Hole _ _ _ _ _ => true | _ => false end.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker