proposition: Lemma augment_with_clauses_correct : forall cl st (WF: wf_state st) (CL: has_conflict_clause (hconsmap st) cl), ((hconsmap_progress (augment_with_clause cl) st /\ wf_result_state (augment_with_clause cl st) /\ (eval_state st -> eval_literal_list cl -> eval_result_state (augment_with_clause cl st)) /\ (eval_annot_state st -> eval_literal_list cl -> eval_annot_result_state (augment_with_clause cl st)))).
proof: Proof. intros. split_and. - apply hconsmap_augment_with_clause; auto. - apply wf_augment_with_clause;auto. - apply eval_augment_with_clause; auto. - apply eval_annot_augment_with_clause;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause