sig
  val mk_sort : Z3.context -> Z3.Sort.sort
  val get_big_int : Z3.Expr.expr -> Z.t
  val numeral_to_string : Z3.Expr.expr -> string
  val mk_const : Z3.context -> Z3.Symbol.symbol -> Z3.Expr.expr
  val mk_const_s : Z3.context -> string -> Z3.Expr.expr
  val mk_mod : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_rem : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_numeral_s : Z3.context -> string -> Z3.Expr.expr
  val mk_numeral_i : Z3.context -> int -> Z3.Expr.expr
  val mk_int2real : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_int2bv : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
end