sig
  type t
  type operator = Plus | Minus | Mult | Div | Modulo
  val make_int : Num.num -> Smt.Term.t
  val make_real : Num.num -> Smt.Term.t
  val make_app : Smt.Symbol.t -> Smt.Term.t list -> Smt.Term.t
  val make_arith :
    Smt.Term.operator -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
  val make_ite : Smt.Formula.t -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
  val is_int : Smt.Term.t -> bool
  val is_real : Smt.Term.t -> bool
  val t_true : Smt.Term.t
  val t_false : Smt.Term.t
end