sig
  val mk_sort : Z3.context -> int -> Z3.Sort.sort
  val is_bv : Z3.Expr.expr -> bool
  val is_bv_numeral : Z3.Expr.expr -> bool
  val is_bv_bit1 : Z3.Expr.expr -> bool
  val is_bv_bit0 : Z3.Expr.expr -> bool
  val is_bv_uminus : Z3.Expr.expr -> bool
  val is_bv_add : Z3.Expr.expr -> bool
  val is_bv_sub : Z3.Expr.expr -> bool
  val is_bv_mul : Z3.Expr.expr -> bool
  val is_bv_sdiv : Z3.Expr.expr -> bool
  val is_bv_udiv : Z3.Expr.expr -> bool
  val is_bv_SRem : Z3.Expr.expr -> bool
  val is_bv_urem : Z3.Expr.expr -> bool
  val is_bv_smod : Z3.Expr.expr -> bool
  val is_bv_sdiv0 : Z3.Expr.expr -> bool
  val is_bv_udiv0 : Z3.Expr.expr -> bool
  val is_bv_srem0 : Z3.Expr.expr -> bool
  val is_bv_urem0 : Z3.Expr.expr -> bool
  val is_bv_smod0 : Z3.Expr.expr -> bool
  val is_bv_ule : Z3.Expr.expr -> bool
  val is_bv_sle : Z3.Expr.expr -> bool
  val is_bv_uge : Z3.Expr.expr -> bool
  val is_bv_sge : Z3.Expr.expr -> bool
  val is_bv_ult : Z3.Expr.expr -> bool
  val is_bv_slt : Z3.Expr.expr -> bool
  val is_bv_ugt : Z3.Expr.expr -> bool
  val is_bv_sgt : Z3.Expr.expr -> bool
  val is_bv_and : Z3.Expr.expr -> bool
  val is_bv_or : Z3.Expr.expr -> bool
  val is_bv_not : Z3.Expr.expr -> bool
  val is_bv_xor : Z3.Expr.expr -> bool
  val is_bv_nand : Z3.Expr.expr -> bool
  val is_bv_nor : Z3.Expr.expr -> bool
  val is_bv_xnor : Z3.Expr.expr -> bool
  val is_bv_concat : Z3.Expr.expr -> bool
  val is_bv_signextension : Z3.Expr.expr -> bool
  val is_bv_zeroextension : Z3.Expr.expr -> bool
  val is_bv_extract : Z3.Expr.expr -> bool
  val is_bv_repeat : Z3.Expr.expr -> bool
  val is_bv_reduceor : Z3.Expr.expr -> bool
  val is_bv_reduceand : Z3.Expr.expr -> bool
  val is_bv_comp : Z3.Expr.expr -> bool
  val is_bv_shiftleft : Z3.Expr.expr -> bool
  val is_bv_shiftrightlogical : Z3.Expr.expr -> bool
  val is_bv_shiftrightarithmetic : Z3.Expr.expr -> bool
  val is_bv_rotateleft : Z3.Expr.expr -> bool
  val is_bv_rotateright : Z3.Expr.expr -> bool
  val is_bv_rotateleftextended : Z3.Expr.expr -> bool
  val is_bv_rotaterightextended : Z3.Expr.expr -> bool
  val is_int2bv : Z3.Expr.expr -> bool
  val is_bv2int : Z3.Expr.expr -> bool
  val is_bv_carry : Z3.Expr.expr -> bool
  val is_bv_xor3 : Z3.Expr.expr -> bool
  val get_size : Z3.Sort.sort -> int
  val numeral_to_string : Z3.Expr.expr -> string
  val mk_const : Z3.context -> Z3.Symbol.symbol -> int -> Z3.Expr.expr
  val mk_const_s : Z3.context -> string -> int -> Z3.Expr.expr
  val mk_not : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_redand : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_redor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_and : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_or : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_xor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_nand : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_nor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_xnor : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_neg : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_add : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sub : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_mul : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_udiv : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sdiv : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_urem : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_srem : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_smod : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ult : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_slt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ule : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sle : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_uge : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sge : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ugt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sgt : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_concat : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_extract : Z3.context -> int -> int -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sign_ext : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_zero_ext : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_repeat : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_shl : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_lshr : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ashr : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_rotate_left : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_rotate_right : Z3.context -> int -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ext_rotate_left :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_ext_rotate_right :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_bv2int : Z3.context -> Z3.Expr.expr -> bool -> Z3.Expr.expr
  val mk_add_no_overflow :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> bool -> Z3.Expr.expr
  val mk_add_no_underflow :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sub_no_overflow :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_sub_no_underflow :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> bool -> Z3.Expr.expr
  val mk_sdiv_no_overflow :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_neg_no_overflow : Z3.context -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_mul_no_overflow :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> bool -> Z3.Expr.expr
  val mk_mul_no_underflow :
    Z3.context -> Z3.Expr.expr -> Z3.Expr.expr -> Z3.Expr.expr
  val mk_numeral : Z3.context -> string -> int -> Z3.Expr.expr
end