sig
  val init : (UfSymbol.t -> unit) -> TransSys.t -> unit
  val incr_k : unit -> unit
  val check_and_block :
    (UfSymbol.t -> unit) -> TransSys.t -> Model.path -> Term.t list
end