diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle index 4b93bf2cdabc14eb1c5cafcdce5977f539c35468..d4f8bf7081dfdf956b37a1f15fcbc2a32b1d2d6a 100644 --- a/tests/bugs/oracle/term.res.oracle +++ b/tests/bugs/oracle/term.res.oracle @@ -3,11 +3,16 @@ Now output intermediate result [wp] Running WP plugin... [wp] Warning: Missing RTE guards +[wp] [CFG] Goal Z2m2_terminates : Valid (Trivial) +[wp] [CFG] Goal Z2m3_terminates : Valid (Trivial) +[wp] [CFG] Goal Z2m4_terminates : Valid (Trivial) +[wp] [CFG] Goal Z3m3a_terminates : Valid (Trivial) +[wp] [CFG] Goal Z3m3b_terminates : Valid (Trivial) [wp] 3 goals scheduled [wp] [Qed] Goal typed_Z2m2_ensures : Valid [wp] [Qed] Goal typed_Z2m3_c_ensures : Valid [wp] [Qed] Goal typed_Z3m3a_c_ensures : Valid -[wp] Proved goals: 3 / 3 +[wp] Proved goals: 8 / 8 Qed: 3 /* Generated by Frama-C */ /*@ behavior c: