sig
  type dnf = Types.SAtom.t list
  type type_constructors = Hstring.t * Hstring.t list
  type swts = (Types.SAtom.t * Types.Term.t) list
  type glob_update = UTerm of Types.Term.t | UCase of Ast.swts
  type update = {
    up_loc : Util.loc;
    up_arr : Hstring.t;
    up_arg : Variable.t list;
    up_swts : Ast.swts;
  }
  type transition_info = {
    tr_name : Hstring.t;
    tr_args : Variable.t list;
    tr_reqs : Types.SAtom.t;
    tr_ureq : (Variable.t * Ast.dnf) list;
    tr_lets : (Hstring.t * Types.Term.t) list;
    tr_assigns : (Hstring.t * Ast.glob_update) list;
    tr_upds : Ast.update list;
    tr_nondets : Hstring.t list;
    tr_loc : Util.loc;
  }
  type transition_func =
      Types.Term.t -> Types.op_comp -> Types.Term.t -> Types.Atom.t
  type transition = {
    tr_info : Ast.transition_info;
    tr_tau : Ast.transition_func;
    tr_reset : unit -> unit;
  }
  type system = {
    globals : (Util.loc * Hstring.t * Smt.Type.t) list;
    consts : (Util.loc * Hstring.t * Smt.Type.t) list;
    arrays : (Util.loc * Hstring.t * (Smt.Type.t list * Smt.Type.t)) list;
    type_defs : (Util.loc * Ast.type_constructors) list;
    init : Util.loc * Variable.t list * Ast.dnf;
    invs : (Util.loc * Variable.t list * Types.SAtom.t) list;
    unsafe : (Util.loc * Variable.t list * Types.SAtom.t) list;
    trans : Ast.transition_info list;
  }
  type kind = Approx | Orig | Node | Inv
  type node_cube = {
    cube : Cube.t;
    tag : int;
    kind : Ast.kind;
    depth : int;
    mutable deleted : bool;
    from : Ast.trace;
  }
  and trace_step = Ast.transition_info * Variable.t list * Ast.node_cube
  and trace = Ast.trace_step list
  type init_instance = {
    init_cdnf : Ast.dnf list;
    init_cdnf_a : Types.ArrayAtom.t list list;
    init_invs : Types.ArrayAtom.t list;
  }
  type t_system = {
    t_globals : Hstring.t list;
    t_consts : Hstring.t list;
    t_arrays : Hstring.t list;
    t_init : Variable.t list * Ast.dnf;
    t_init_instances : (int, Ast.init_instance) Hashtbl.t;
    t_invs : Ast.node_cube list;
    t_unsafe : Ast.node_cube list;
    t_trans : Ast.transition list;
  }
end