sig
  val main_bool :
    bool -> 'InputSystem.t -> Analysis.param -> TransSys.t -> unit
  val main_int :
    bool -> 'InputSystem.t -> Analysis.param -> TransSys.t -> unit
  val main_real :
    bool -> 'InputSystem.t -> Analysis.param -> TransSys.t -> unit
  val exit : '-> unit
  module type Out =
    sig
      val main :
        Numeral.t option ->
        bool ->
        bool ->
        bool ->
        'InputSystem.t ->
        Analysis.param ->
        TransSys.t -> (TransSys.t * Term.TermSet.t * Term.TermSet.t) list
      val exit : '-> unit
    end
  module BoolInvGen : Out
  module IntInvGen : Out
  module RealInvGen : Out
  module EqOnly :
    sig
      module BoolInvGen : Out
      module IntInvGen : Out
      module RealInvGen : Out
    end
end