let print_report ~safe visited candidates = print_candidates ~safe candidates; Pretty.print_title std_formatter "STATS"; printf "Number of visited nodes : %d@." !cpt_nodes; printf "Fixpoints : %d@." !cpt_fix; printf "Number of solver calls : %d@." (Prover.SMT.get_calls ()); printf "Max Number of processes : %d@." !cpt_process; if Options.delete then printf "Number of deleted nodes : %d@." !cpt_delete; if do_brab then printf "Number of %s : %d@." (if safe then "invariants" else "candidates") (List.length candidates); printf "Restarts : @[%d%a@]@." !cpt_restart print_rounds_nb (); if profiling then begin printf "%a" Pretty.print_line (); print_time_pre (); print_time_fix (); print_time_rp (); print_time_simpl (); print_time_subset (); print_time_apply (); print_time_sort (); print_time_formulas (); print_time_prover (); print_time_forward (); print_time_ccheck (); end; printf "%a" Pretty.print_double_line ()