sig
  type model
  module FuncInterp :
    sig
      type func_interp
      module FuncEntry :
        sig
          type func_entry
          val get_value :
            Z3.Model.FuncInterp.FuncEntry.func_entry -> Z3.Expr.expr
          val get_num_args : Z3.Model.FuncInterp.FuncEntry.func_entry -> int
          val get_args :
            Z3.Model.FuncInterp.FuncEntry.func_entry -> Z3.Expr.expr list
          val to_string : Z3.Model.FuncInterp.FuncEntry.func_entry -> string
        end
      val get_num_entries : Z3.Model.FuncInterp.func_interp -> int
      val get_entries :
        Z3.Model.FuncInterp.func_interp ->
        Z3.Model.FuncInterp.FuncEntry.func_entry list
      val get_else : Z3.Model.FuncInterp.func_interp -> Z3.Expr.expr
      val get_arity : Z3.Model.FuncInterp.func_interp -> int
      val to_string : Z3.Model.FuncInterp.func_interp -> string
    end
  val get_const_interp :
    Z3.Model.model -> Z3.FuncDecl.func_decl -> Z3.Expr.expr option
  val get_const_interp_e :
    Z3.Model.model -> Z3.Expr.expr -> Z3.Expr.expr option
  val get_func_interp :
    Z3.Model.model ->
    Z3.FuncDecl.func_decl -> Z3.Model.FuncInterp.func_interp option
  val get_num_consts : Z3.Model.model -> int
  val get_const_decls : Z3.Model.model -> Z3.FuncDecl.func_decl list
  val get_num_funcs : Z3.Model.model -> int
  val get_func_decls : Z3.Model.model -> Z3.FuncDecl.func_decl list
  val get_decls : Z3.Model.model -> Z3.FuncDecl.func_decl list
  val eval : Z3.Model.model -> Z3.Expr.expr -> bool -> Z3.Expr.expr option
  val evaluate :
    Z3.Model.model -> Z3.Expr.expr -> bool -> Z3.Expr.expr option
  val get_num_sorts : Z3.Model.model -> int
  val get_sorts : Z3.Model.model -> Z3.Sort.sort list
  val sort_universe : Z3.Model.model -> Z3.Sort.sort -> Z3.Expr.expr list
  val to_string : Z3.Model.model -> string
end