sig
  type base
  val kill_base : LockStepDriver.base -> unit
  val mk_base_checker : TransSys.t -> Numeral.t -> LockStepDriver.base
  val base_add_invariants :
    LockStepDriver.base -> bool -> Term.t list -> unit
  val query_base : LockStepDriver.base -> Term.t list -> Model.t option
  type step
  val kill_step : LockStepDriver.step -> unit
  val to_step : LockStepDriver.base -> LockStepDriver.step
  val step_cert : LockStepDriver.step -> int
  val step_add_invariants :
    LockStepDriver.step -> bool -> Term.t list -> unit
  val query_step :
    bool -> LockStepDriver.step -> (Term.t * 'a) list -> (Term.t * 'a) list
  val nu_query_step :
    bool -> LockStepDriver.step -> Term.t list -> Model.t option
  type pruning
  val pruning_sys : LockStepDriver.pruning -> TransSys.t
  val kill_pruning : LockStepDriver.pruning -> unit
  val mk_pruning_checker : TransSys.t -> LockStepDriver.pruning
  val pruning_add_invariants :
    LockStepDriver.pruning -> bool -> Term.t list -> unit
  val query_pruning :
    LockStepDriver.pruning -> Term.t list -> Term.t list * Term.t list
end