package mc2

  1. Overview
  2. Docs
type t = [ `UNSAT ] state
val unsat_conflict : t -> Mc2_core__.Solver_types.clause

Returns the unsat clause found at the toplevel

val get_proof : t -> proof

returns a persistent proof of the empty clause from the Unsat result.