diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml index 38e73ded32b279bd105fbbd4848bc61e7ea326b5..61230201355a42ea080a7dcd676971d9832c62cf 100644 --- a/src/plugins/wp/ProverWhy3.ml +++ b/src/plugins/wp/ProverWhy3.ml @@ -323,6 +323,13 @@ end (* --- Assembling Goal --- *) (* -------------------------------------------------------------------------- *) +let sanitize_expl fmt title = + for i = 0 to String.length title - 1 do + match title.[i] with + | '\n' | '\t' -> Format.pp_print_char fmt ' ' + | c -> Format.pp_print_char fmt c + done + let assemble_goal ~id ~title ~theory ?axioms prop fmt = (** Also create the directory *) let goal = cluster ~id ~title () in @@ -348,9 +355,9 @@ let assemble_goal ~id ~title ~theory ?axioms prop fmt = engine#set_goal true ; engine#global begin fun () -> - v#printf "@[<hv 2>goal %s[@expl:%s]:@ %a@]@\n@\n" + v#printf "@[<hv 2>goal %s[@expl:%a]:@ %a@]@\n@\n" why3_goal_name - title + sanitize_expl title engine#pp_prop (F.e_prop prop) ; end ; engine#set_goal false ;