sig
  type t = int * Term.t
  type symbols = {
    phi : string;
    init : string;
    prop : string;
    trans : string;
  }
  type out = {
    k : int;
    names : Certificate.symbols;
    dirname : string;
    proofname : string;
    base : string;
    induction : string;
    implication : string;
    dummy_trace : string;
  }
  type system = {
    names : Certificate.symbols;
    smt2_file : string;
    smt2_lfsc_trace_file : string;
  }
  type invariant = {
    k : int;
    name : string;
    dirname : string;
    phi_file : string;
    phi_lfsc_trace_file : string;
    base : string;
    induction : string;
    implication : string;
    for_system : Certificate.system;
    kind2_system : Certificate.system;
    jkind_system : Certificate.system;
    obs_system : Certificate.system;
  }
  val merge : Certificate.t list -> Certificate.t
  val split : Certificate.t -> Certificate.t list
  val split_certs : Certificate.t list -> Certificate.t list
  val size : Certificate.t -> int
end