sig
  type model = Model.t
  type term = Term.t
  type num = Numeral.t
  type depth = TestgenTree.num
  type mode = Scope.t
  type mode_conj = TestgenTree.mode list * TestgenTree.mode list
  type mode_path = TestgenTree.mode_conj list
  type t
  exception TopReached
  val mk :
    (TestgenTree.mode -> TestgenTree.term) ->
    TestgenTree.mode_conj -> TestgenTree.t
  val mode_path_of : TestgenTree.t -> TestgenTree.mode_path
  val path_of : TestgenTree.t -> Term.t
  val blocking_path_of : TestgenTree.t -> Term.t
  val depth_of : TestgenTree.t -> TestgenTree.num
  val push : TestgenTree.t -> TestgenTree.mode_conj -> unit
  val pop : TestgenTree.t -> unit
  val update : TestgenTree.t -> TestgenTree.mode_conj -> unit
  val pp_print_tree : Format.formatter -> TestgenTree.t -> unit
end