sig
  val symbol : ('b, 'a) ZZ3_sigs.S.symbol -> 'a ZZ3_sigs.S.term
  val simplify :
    ?params:Z3.Params.params -> 'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
  val eq :
    'a ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val distinct :
    'a ZZ3_sigs.S.term list -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ite :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    ([< ZZ3_sigs.S.zany ] as 'a) ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
  val int : int -> [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
  val bigint : Z.t -> [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
  val rat : Q.t -> [> ZZ3_sigs.S.zreal ] ZZ3_sigs.S.term
  val i2q :
    [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zreal ] ZZ3_sigs.S.term
  val q2i :
    [< ZZ3_sigs.S.zreal ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
  val true_ : [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val false_ : [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val bool : bool -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val and_ :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term list ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val or_ :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term list ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val not :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val imply :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val iff :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val xor :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ge :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val le :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val gt :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val lt :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val neg :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
  val add :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term list -> 'a ZZ3_sigs.S.term
  val sub :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term list -> 'a ZZ3_sigs.S.term
  val mul :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term list -> 'a ZZ3_sigs.S.term
  val ixor :
    [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
  val div :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
  val mod_ :
    [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
  val rem :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.znum ] ZZ3_sigs.S.term
  val ( ! ) : ('b, 'a) ZZ3_sigs.S.symbol -> 'a ZZ3_sigs.S.term
  val ( = ) :
    'a ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( <> ) :
    'a ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( && ) :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( || ) :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( <=> ) :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( ==> ) :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( lxor ) :
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( < ) :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( <= ) :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( > ) :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( >= ) :
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
  val ( + ) :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
  val ( - ) :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
  val ( * ) :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
  val ( / ) :
    ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
    'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
  val ( mod ) :
    [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
    [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
    [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
  val with_typ : ('a, 'b) ZZ3_sigs.S.typ -> 'a -> 'b ZZ3_sigs.S.term
  val to_string : 'a ZZ3_sigs.S.term -> string
  val raw : 'a ZZ3_sigs.S.term -> Z3.Expr.expr
end