sig
  type t
  val mk : TransSys.t -> TestgenSolver.t
  val rm : TestgenSolver.t -> unit
  val restart : TestgenSolver.t -> TestgenSolver.t
  val comment : TestgenSolver.t -> string -> unit
  val checksat :
    TestgenSolver.t ->
    Numeral.t ->
    Term.t ->
    Term.t list ->
    ('a * Term.t) list ->
    (SMTSolver.t -> 'b) -> (('a * Term.t) list * 'b) option
end