sig
  val generalize :
    TransSys.t ->
    (UfSymbol.t * (Var.t list * Term.t)) list ->
    Model.t -> Var.t list -> Term.t -> Term.t list
  val on_exit : unit -> unit
end