sig
  val produce_assignments : bool
  val produce_cores : bool
  val produce_proofs : bool
  val logic : TermLib.logic
  val id : int
end