sig
  type z3_context = Z3.context
  type z3_expr = Z3.Expr.expr
  type z3_func_decl = Z3.FuncDecl.func_decl
  type 'a open_expr =
      [ `Add of 'a list
      | `And of 'a list
      | `App of SrkZ3.z3_func_decl * 'a list
      | `Atom of [ `Eq | `Leq | `Lt ] * 'a * 'a
      | `Binop of [ `Div | `Mod ] * 'a * 'a
      | `Fls
      | `Ite of 'a * 'a * 'a
      | `Mul of 'a list
      | `Not of 'a
      | `Or of 'a list
      | `Quantify of [ `Exists | `Forall ] * string * Syntax.typ_fo * 'a
      | `Real of QQ.t
      | `Tru
      | `Unop of [ `Floor | `Neg ] * 'a
      | `Var of int * Syntax.typ_fo ]
  val z3_of_term :
    'a Syntax.context -> SrkZ3.z3_context -> 'a Syntax.term -> SrkZ3.z3_expr
  val z3_of_formula :
    'a Syntax.context ->
    SrkZ3.z3_context -> 'a Syntax.formula -> SrkZ3.z3_expr
  val z3_of_expr :
    'a Syntax.context ->
    SrkZ3.z3_context -> ('a, Syntax.typ_fo) Syntax.expr -> SrkZ3.z3_expr
  val term_of_z3 : 'a Syntax.context -> SrkZ3.z3_expr -> 'a Syntax.term
  val formula_of_z3 : 'a Syntax.context -> SrkZ3.z3_expr -> 'a Syntax.formula
  val expr_of_z3 :
    'a Syntax.context -> SrkZ3.z3_expr -> ('a, Syntax.typ_fo) Syntax.expr
  module Solver :
    sig
      type 'a t
      val add : 'a SrkZ3.Solver.t -> 'a Syntax.formula list -> unit
      val push : 'a SrkZ3.Solver.t -> unit
      val pop : 'a SrkZ3.Solver.t -> int -> unit
      val reset : 'a SrkZ3.Solver.t -> unit
      val check :
        'a SrkZ3.Solver.t ->
        'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
      val to_string : 'a SrkZ3.Solver.t -> string
      val get_model :
        ?symbols:Syntax.symbol list ->
        'a SrkZ3.Solver.t ->
        [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
      val get_concrete_model :
        'a SrkZ3.Solver.t ->
        Syntax.symbol list ->
        [ `Sat of 'a Interpretation.interpretation | `Unknown | `Unsat ]
      val get_unsat_core :
        'a SrkZ3.Solver.t ->
        'a Syntax.formula list ->
        [ `Sat | `Unknown | `Unsat of 'a Syntax.formula list ]
    end
  val mk_solver :
    ?context:SrkZ3.z3_context ->
    ?theory:string -> 'a Syntax.context -> 'a SrkZ3.Solver.t
  val optimize_box :
    ?context:SrkZ3.z3_context ->
    'a Syntax.context ->
    'a Syntax.formula ->
    'a Syntax.term list -> [ `Sat of Interval.t list | `Unknown | `Unsat ]
  val qe :
    ?context:SrkZ3.z3_context ->
    'a Syntax.context -> 'a Syntax.formula -> 'a Syntax.formula
  val load_smtlib2 :
    ?context:SrkZ3.z3_context ->
    'a Syntax.context -> string -> 'a Syntax.formula
  val interpolate_seq :
    ?context:SrkZ3.z3_context ->
    'a Syntax.context ->
    'a Syntax.formula list ->
    [ `Sat of 'a Interpretation.interpretation
    | `Unknown
    | `Unsat of 'a Syntax.formula list ]
  module CHC :
    sig
      type 'a solver
      val mk_solver :
        ?context:SrkZ3.z3_context -> 'a Syntax.context -> 'a SrkZ3.CHC.solver
      val register_relation : 'a SrkZ3.CHC.solver -> Syntax.symbol -> unit
      val add_rule :
        'a SrkZ3.CHC.solver -> 'a Syntax.formula -> 'a Syntax.formula -> unit
      val add : 'a SrkZ3.CHC.solver -> 'a Syntax.formula list -> unit
      val check :
        'a SrkZ3.CHC.solver ->
        'a Syntax.formula list -> [ `Sat | `Unknown | `Unsat ]
      val get_solution :
        'a SrkZ3.CHC.solver -> Syntax.symbol -> 'a Syntax.formula
      val to_string : 'a SrkZ3.CHC.solver -> string
      val push : 'a SrkZ3.CHC.solver -> unit
      val pop : 'a SrkZ3.CHC.solver -> unit
    end
end