From b6323d44694cd51a113808b4a8808b442569598e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 7 Sep 2020 14:47:44 +0200
Subject: [PATCH] [tests] update test case for generalized check

---
 tests/spec/generalized_check.i                 |  3 +++
 tests/spec/oracle/generalized_check.res.oracle | 11 +++++++++++
 2 files changed, 14 insertions(+)

diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 1409e3efc7a..856e33415fc 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 7017e6e7b84..eefae9d2492 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;
  */
-- 
GitLab