proposition: Lemma wf_generate_conflict_clause : forall [st g] (WF: wf_state st) (HASG: has_oform (hconsmap st) g), Forall (has_literal (hconsmap st)) (generate_conflict_clause st g).
proof: Proof. unfold generate_conflict_clause. intros. destruct WF. destruct (extract_theory_problem (hconsmap st) (units st)) as (ln,lp) eqn:EQ. apply wf_extract_thy_pb in EQ; auto. destruct EQ as (C1 & C2). specialize (wf_add_conclusion C1 C2 HASG). destruct (add_conclusion g (ln,lp)) as (ln1,lp1). simpl. intros (C1' & C2'). repeat rewrite Forall_app. repeat split ; auto. apply wf_collect_all_wneg; auto. apply wf_units_weaken; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause