sig
  type sys = TransSys.t
  type svar = StateVar.t
  type actlit = UfSymbol.t
  type term = Term.t
  type model = Model.t
  type values = (Term.t * Term.t) list
  type k = Numeral.t
  val term_of : TestgenLib.actlit -> TestgenLib.term
  val list_eq : 'a list -> 'a list -> bool
  type 'data context = {
    sys : TestgenLib.sys;
    declare : TestgenLib.actlit -> unit;
    actlit_implications :
      ?eq:bool -> (TestgenLib.actlit * TestgenLib.term) list -> unit;
    checksat_getvalues :
      TestgenLib.actlit list ->
      TestgenLib.term list -> TestgenLib.values option;
    trace_comment : string -> unit;
    mutable data : 'data;
  }
  val mk_context :
    'data ->
    TestgenLib.sys ->
    (TestgenLib.actlit -> unit) ->
    (?eq:bool -> (TestgenLib.actlit * TestgenLib.term) list -> unit) ->
    (TestgenLib.actlit list ->
     TestgenLib.term list -> TestgenLib.values option) ->
    (string -> unit) -> 'data TestgenLib.context
  val declare : 'data TestgenLib.context -> TestgenLib.actlit -> unit
  val activate :
    'data TestgenLib.context ->
    ?eq:bool -> (TestgenLib.actlit * TestgenLib.term) list -> unit
  val get_values :
    'data TestgenLib.context ->
    TestgenLib.actlit list ->
    TestgenLib.term list -> TestgenLib.values option
  val comment : 'data TestgenLib.context -> string -> unit
  val cex_to_inputs_csv :
    Format.formatter ->
    TestgenLib.sys -> TestgenLib.model -> TestgenLib.k -> unit
  val cex_to_outputs_csv :
    Format.formatter ->
    TestgenLib.sys -> TestgenLib.model -> TestgenLib.k -> unit
  type contract_testcase = (TestgenLib.k * TestgenLib.svar list) list
  type contract_testcases =
      (TestgenLib.actlit * TestgenLib.k * TestgenLib.contract_testcase) list
  val pp_print_contract_testcase :
    Format.formatter -> TestgenLib.contract_testcase -> unit
  val pp_print_contract_testcase_named :
    TestgenLib.sys ->
    Format.formatter -> TestgenLib.contract_testcase -> unit
  val pp_print_contract_testcases :
    Format.formatter -> TestgenLib.contract_testcases -> unit
  val pp_print_contract_testcases_named :
    TestgenLib.sys ->
    Format.formatter -> TestgenLib.contract_testcases -> unit
  val description_of_contract_testcase :
    TestgenLib.sys ->
    TestgenLib.actlit * TestgenLib.k * TestgenLib.contract_testcase ->
    string list
  type tree =
      Branch of (string list * TestgenLib.tree) list
    | Leaf of string list list
  val pp_print_tree : Format.formatter -> TestgenLib.tree -> unit
  val testcases_to_tree :
    TestgenLib.sys -> TestgenLib.contract_testcases -> TestgenLib.tree
  val unroll_test_case :
    TestgenLib.contract_testcase ->
    TestgenLib.k ->
    TestgenLib.contract_testcase -> TestgenLib.contract_testcase
  val extend_contract_testcases :
    TestgenLib.contract_testcases TestgenLib.context ->
    TestgenLib.k -> TestgenLib.contract_testcases
  val testcase_gen :
    string ->
    string ->
    (string -> string -> string -> string list -> 'a) ->
    TestgenLib.contract_testcases TestgenLib.context ->
    (TestgenLib.actlit list -> TestgenLib.model option) -> unit
end