fact: Definition ProverT := state -> option HFormula -> result state (hmap * list conflict_clause * LitSet.t).
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause