sig
  type t
  type id
  type location
  val const :
    ?loc:Ast_smtlib.Term.location -> Ast_smtlib.Term.id -> Ast_smtlib.Term.t
  val int : ?loc:Ast_smtlib.Term.location -> string -> Ast_smtlib.Term.t
  val real : ?loc:Ast_smtlib.Term.location -> string -> Ast_smtlib.Term.t
  val hexa : ?loc:Ast_smtlib.Term.location -> string -> Ast_smtlib.Term.t
  val binary : ?loc:Ast_smtlib.Term.location -> string -> Ast_smtlib.Term.t
  val colon :
    ?loc:Ast_smtlib.Term.location ->
    Ast_smtlib.Term.t -> Ast_smtlib.Term.t -> Ast_smtlib.Term.t
  val apply :
    ?loc:Ast_smtlib.Term.location ->
    Ast_smtlib.Term.t -> Ast_smtlib.Term.t list -> Ast_smtlib.Term.t
  val letin :
    ?loc:Ast_smtlib.Term.location ->
    Ast_smtlib.Term.t list -> Ast_smtlib.Term.t -> Ast_smtlib.Term.t
  val forall :
    ?loc:Ast_smtlib.Term.location ->
    Ast_smtlib.Term.t list -> Ast_smtlib.Term.t -> Ast_smtlib.Term.t
  val exists :
    ?loc:Ast_smtlib.Term.location ->
    Ast_smtlib.Term.t list -> Ast_smtlib.Term.t -> Ast_smtlib.Term.t
  val sexpr :
    ?loc:Ast_smtlib.Term.location ->
    Ast_smtlib.Term.t list -> Ast_smtlib.Term.t
  val annot :
    ?loc:Ast_smtlib.Term.location ->
    Ast_smtlib.Term.t -> Ast_smtlib.Term.t list -> Ast_smtlib.Term.t
end