sig
  type goal
  val get_precision : Z3.Goal.goal -> Z3enums.goal_prec
  val is_precise : Z3.Goal.goal -> bool
  val is_underapproximation : Z3.Goal.goal -> bool
  val is_overapproximation : Z3.Goal.goal -> bool
  val is_garbage : Z3.Goal.goal -> bool
  val add : Z3.Goal.goal -> Z3.Expr.expr list -> unit
  val is_inconsistent : Z3.Goal.goal -> bool
  val get_depth : Z3.Goal.goal -> int
  val reset : Z3.Goal.goal -> unit
  val get_size : Z3.Goal.goal -> int
  val get_formulas : Z3.Goal.goal -> Z3.Expr.expr list
  val get_num_exprs : Z3.Goal.goal -> int
  val is_decided_sat : Z3.Goal.goal -> bool
  val is_decided_unsat : Z3.Goal.goal -> bool
  val translate : Z3.Goal.goal -> Z3.context -> Z3.Goal.goal
  val simplify : Z3.Goal.goal -> Z3.Params.params option -> Z3.Goal.goal
  val mk_goal : Z3.context -> bool -> bool -> bool -> Z3.Goal.goal
  val to_string : Z3.Goal.goal -> string
  val as_expr : Z3.Goal.goal -> Z3.Expr.expr
end