let pp pp fmt status =
    let ppj fmt rho =
      if !pp_justification then
        begin
          Pretty.string fmt "\n";
          Jst.pp fmt rho
        end
    in
      match status with
        | Valid(rho) -> 
            Pretty.apply ppj fmt (":valid", [rho])
        | Inconsistent(rho) -> 
            Pretty.apply ppj fmt (":unsat", [rho])
        | Ok(x) -> 
            Pretty.apply pp fmt (":ok ", [x])