diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml index 06d51a31f719bc16929b398f13fb724df980582e..c9595b573140955eb7832839c5b33397d2593d8d 100644 --- a/src/plugins/wp/register.ml +++ b/src/plugins/wp/register.ml @@ -369,7 +369,7 @@ let do_wpo_success ~shell ~updating goal success = | None -> () | Some prover -> Wp_parameters.feedback ~ontty:`Silent - "[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal) + "[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover else if Wpo.is_smoke_test goal then begin match success with diff --git a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle index a83d4680fb04a7a5685595e42814541d3a0078d8..366ce2207261b201113ed48f6f52600bd8224b9e 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle @@ -3,9 +3,9 @@ [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 4 goals scheduled -[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid -[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid -[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid +[wp] [Generated] Goal typed_u8_is_continue_assigns_part3 (Qed) +[wp] [Generated] Goal typed_u8_is_continue_assigns_part2 (Qed) +[wp] [Generated] Goal typed_u8_is_continue_assigns_part1 (Qed) [wp] 4 goals generated ------------------------------------------------------------ Function u8_is_continue