sig
  val has_division_by_zero_happened : unit -> bool
  val simplify_term :
    (UfSymbol.t * (Var.t list * Term.t)) list -> Term.t -> Term.t
  val simplify_term_model :
    ?default_of_var:(Var.t -> Term.t) ->
    (UfSymbol.t * (Var.t list * Term.t)) list -> Model.t -> Term.t -> Term.t
end