fact: Record wf_state (st : state) : Prop := { wf_hm : wf (hconsmap st); wf_arrows : List.Forall (has_literal (hconsmap st)) (arrows st) ; wf_wn_m : wf_map (wneg st); wf_wneg : wf_units_def (wneg st) (hconsmap st); wf_units : wf_units_lit (units st) (hconsmap st); wf_stack : List.Forall (check_annot has_literal (hconsmap st)) (unit_stack st); wf_clauses : has_clauses (hconsmap st) (clauses st); wf_units_m : wf_map (units st); wf_clauses_m : WMap.wf (clauses st); }.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause