proposition: Lemma resolution_checker_correct : forall rho, Valuation.wf rho -> forall s t cid, resolution_checker C.is_false s t cid-> ~S.valid rho s.
proof: Proof. intros rho Hwr; apply _checker__correct. intros; apply C.is_false_correct; trivial. intros s Hv (pos, r); apply S.valid_set_resolve; trivial. Qed.
imports: Bool Int63 PArray Misc State SMT_terms Syntactic Arithmetic Operators Assumptions Cnf Euf Lia BVList Bva_checker Array_checker