proposition: Lemma checker_ext_correct : forall d used_roots c, checker_ext d used_roots c = true -> forall t_i t_func, Atom.wt t_i t_func t_atom -> ~ Euf_Checker.valid t_func t_atom t_form d.
proof: Proof. unfold checker_ext. intros d used_roots (nclauses, t, confl). rewrite !andb_true_iff. intros [[H1 H2] H3] t_i t_func H10 H. eelim checker_correct; try eassumption. apply Euf_Checker.add_roots_correct; try assumption. apply S.valid_make. destruct (Form.check_form_correct (Atom.interp_form_hatom t_i t_func t_atom) (Atom.interp_form_hatom_bv t_i t_func t_atom) _ H1) as [_ H4]; auto with smtcoq_core. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker