sig
  type proof_step = ProofStep.t
  type proof = ProofStep.of_
  type result = Sat | Unsat of proof
  exception WrongState of string
  module type S =
    sig
      module Lit = BBox.Lit
      exception UndecidedLit
      type clause = Lit.t list
      val add_clause : proof:proof_step -> Lit.t list -> unit
      val add_clauses : proof:proof_step -> Lit.t list list -> unit
      val add_clause_seq : proof:proof_step -> Lit.t list Sequence.t -> unit
      val check : unit -> result
      val last_result : unit -> result
      val valuation : Lit.t -> bool
      val valuation_level : Lit.t -> bool * int
      val proved_at_0 : Lit.t -> bool option
      val set_printer : Lit.t CCFormat.printer -> unit
      val get_proof : unit -> proof
      val get_proof_of_lit : Lit.t -> proof
      val setup : unit -> unit
      type save_level
      val root_save_level : save_level
      val save : unit -> save_level
      val restore : save_level -> unit
    end
  module Make : functor (Dummy : sig  end) -> S
end