sig
  type apply_result
  val get_num_subgoals : Z3.Tactic.ApplyResult.apply_result -> int
  val get_subgoals : Z3.Tactic.ApplyResult.apply_result -> Z3.Goal.goal list
  val get_subgoal : Z3.Tactic.ApplyResult.apply_result -> int -> Z3.Goal.goal
  val convert_model :
    Z3.Tactic.ApplyResult.apply_result ->
    int -> Z3.Model.model -> Z3.Model.model
  val to_string : Z3.Tactic.ApplyResult.apply_result -> string
end