fact: Definition success (goal: option HFormula) (lit: IntMap.ptrie (Annot.t bool)) (l:Annot.t literal) := match goal with | None => is_unsat lit l | Some g => if is_goalb g (Annot.elt l) then Some (Annot.deps l) else is_unsat lit l end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause