sig
  type info = { backend : string; time : float; message : string option; }
  type unknown_info =
      U_timeout of Problem.Res.info
    | U_out_of_scope of Problem.Res.info
    | U_incomplete of Problem.Res.info
    | U_other of Problem.Res.info * string
  type ('t, 'ty) t =
      Unsat of Problem.Res.info
    | Sat of ('t, 'ty) Model.t * Problem.Res.info
    | Unknown of Problem.Res.unknown_info list
    | Error of exn * Problem.Res.info
  val mk_info :
    ?message:string ->
    backend:string -> time:float -> unit -> Problem.Res.info
  val map :
    term:('t1 -> 't2) ->
    ty:('ty1 -> 'ty2) ->
    ('t1, 'ty1) Problem.Res.t -> ('t2, 'ty2) Problem.Res.t
  val map_m :
    f:(('t1, 'ty1) Model.t -> ('t2, 'ty2) Model.t) ->
    ('t1, 'ty1) Problem.Res.t -> ('t2, 'ty2) Problem.Res.t
  val print :
    (TermInner.prec -> 't Problem.printer) ->
    'ty Problem.printer -> ('t, 'ty) Problem.Res.t Problem.printer
  val print_info : Problem.Res.info Problem.printer
  val print_unknown_info : Problem.Res.unknown_info Problem.printer
  val print_head : ('a, 'b) Problem.Res.t Problem.printer
  val to_sexp :
    't Problem.to_sexp ->
    'ty Problem.to_sexp -> ('t, 'ty) Problem.Res.t Problem.to_sexp
end