proposition: Lemma checker_b_correct : forall t_var t_form l b c, checker_b t_form l b c = true -> Lit.interp (Form.interp_state_var (PArray.get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l = b.
proof: Proof. unfold checker_b; intros t_var t_form l b c; case b; case_eq (Lit.interp (Form.interp_state_var (get t_var) (fun _ s => BITVECTOR_LIST.zeros s) t_form) l); auto with smtcoq_core; intros H1 H2; elim (checker_correct H2 (rho:=get t_var) (rhobv:=fun _ s => BITVECTOR_LIST.zeros s)); auto with smtcoq_core; rewrite Lit.interp_neg, H1; 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