diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 1409e3efc7af975c24e55cdebc9c4edc3971ab49..856e33415fc3553aeee0e1c4884823a71cb80680 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,3 +1,6 @@
+/* run.config
+OPT: -wp -wp-prover qed -wp-msg-key no-time-info -print
+*/
 /*@ check lemma tauto: \true ==> \true; */
 
 /*@ check requires \valid(x);
diff --git a/tests/spec/oracle/generalized_check.res.oracle b/tests/spec/oracle/generalized_check.res.oracle
index 7017e6e7b8408180fb254621bf34a2de945a6d65..eefae9d2492373d60e0ee4ff279e80dff2cdbd6b 100644
--- a/tests/spec/oracle/generalized_check.res.oracle
+++ b/tests/spec/oracle/generalized_check.res.oracle
@@ -1,4 +1,15 @@
 [kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Qed] Goal typed_f_assigns : Valid
+[wp] [Qed] Goal typed_f_check : Valid
+[wp] [Qed] Goal typed_f_ensures : Valid
+[wp] [Qed] Goal typed_lemma_tauto : Valid
+[wp] [Qed] Goal typed_main_call_f_requires : Valid
+[wp] [Failed] Goal typed_main_check
+[wp] Proved goals:    5 / 6
+  Qed:             5
 /* Generated by Frama-C */
 /*@ check lemma tauto: \true;
  */