proposition: Lemma checker_correct : forall t_form l c, checker t_form l c = true -> forall rho rhobv, ~ (Lit.interp (Form.interp_state_var rho rhobv t_form) l).
proof: Proof. unfold checker; intros t_form l (nclauses, t, confl); unfold is_true; rewrite andb_true_iff; intros [H1 H2] rho rhobv H; apply (cnf_checker_correct (rho:=rho) (rhobv:=rhobv) H1 H2); destruct (Form.check_form_correct rho rhobv _ H1) as [[Ht1 Ht2] Ht3]; apply S.valid_set_clause; auto. apply S.valid_make; auto. unfold C.valid; simpl; rewrite H; auto. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker