sig
  val cache_log :
    pid:Wp.WpPropId.prop_id ->
    model:Wp.WpContext.model ->
    prover:Wp.VCS.prover -> result:Wp.VCS.result -> string
  val pretty :
    pid:Wp.WpPropId.prop_id ->
    model:Wp.WpContext.model ->
    prover:Wp.VCS.prover ->
    result:Wp.VCS.result -> Stdlib.Format.formatter -> unit
  val file_kf :
    kf:Cil_types.kernel_function ->
    model:Wp.WpContext.model -> prover:Wp.VCS.prover -> string
  val file_goal :
    pid:Wp.WpPropId.prop_id ->
    model:Wp.WpContext.model -> prover:Wp.VCS.prover -> string
  val file_logout :
    pid:Wp.WpPropId.prop_id ->
    model:Wp.WpContext.model -> prover:Wp.VCS.prover -> string
  val file_logerr :
    pid:Wp.WpPropId.prop_id ->
    model:Wp.WpContext.model -> prover:Wp.VCS.prover -> string
end