diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i index 7f7c9748c531a7cb0812633335a4ccbd1a73d558..66c93e7d3a8fb3ec726efdd2efa913a36d46b1ba 100644 --- a/tests/spec/generalized_check.i +++ b/tests/spec/generalized_check.i @@ -1,5 +1,5 @@ /* run.config -OPT: -wp -wp-prover qed -wp-msg-key no-cache-info,no-time-info +OPT: -wp -wp-prover qed -wp-msg-key shell OPT: -eva -eva-use-spec f OPT: -print */ diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle index 7f7128dfa8d7a982a69817b1f63a4e4ef677a02b..391634ac903d7d727471bf1b9ed212817085093b 100644 --- a/tests/spec/oracle/generalized_check.0.res.oracle +++ b/tests/spec/oracle/generalized_check.0.res.oracle @@ -1,3 +1,4 @@ +# frama-c -wp [...] [kernel] Parsing tests/spec/generalized_check.i (no preprocessing) [wp] Running WP plugin... [wp] tests/spec/generalized_check.i:30: Warning: