sig
  val to_upper : Z3.Expr.expr -> int -> Z3.Expr.expr
  val to_lower : Z3.Expr.expr -> int -> Z3.Expr.expr
  val to_decimal_string : Z3.Expr.expr -> int -> string
  val numeral_to_string : Z3.Expr.expr -> string
end