diff --git a/tests/ppwp/oracle/expand.res.oracle b/tests/ppwp/oracle/expand.res.oracle index 258b33c6b30c31890252e512ec8fb6d6704812c6..51e6b1b00aa4f235431a697e18b5956a7131af05 100644 --- a/tests/ppwp/oracle/expand.res.oracle +++ b/tests/ppwp/oracle/expand.res.oracle @@ -4,7 +4,6 @@ Now output intermediate result [wp] Warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Qed] Goal typed_Z1m_ensures : Valid -[wp] [Cache] not used [wp] Proved goals: 1 / 1 Qed: 1 /* Generated by Frama-C */ diff --git a/tests/ppwp/oracle/expandf.res.oracle b/tests/ppwp/oracle/expandf.res.oracle index 69cf5301ef8f115b94f1e01fc10ce94a71130ef7..b3239b7f2fa8b4d62398b67070ba5c85c08f1fba 100644 --- a/tests/ppwp/oracle/expandf.res.oracle +++ b/tests/ppwp/oracle/expandf.res.oracle @@ -4,7 +4,6 @@ Now output intermediate result [wp] Warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Qed] Goal typed_Z1m_ensures : Valid -[wp] [Cache] not used [wp] Proved goals: 1 / 1 Qed: 1 /* Generated by Frama-C */ diff --git a/tests/ppwp/oracle/simple.res.oracle b/tests/ppwp/oracle/simple.res.oracle index 6812a5e83bc3307887c3923e97533b2992f8bdcb..80373643d6d335127dec6d90bfba47ce147d4198 100644 --- a/tests/ppwp/oracle/simple.res.oracle +++ b/tests/ppwp/oracle/simple.res.oracle @@ -4,7 +4,6 @@ Now output intermediate result [wp] Warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Qed] Goal typed_Z1m_ensures : Valid -[wp] [Cache] not used [wp] Proved goals: 1 / 1 Qed: 1 /* Generated by Frama-C */ diff --git a/tests/ppwp/oracle/z.res.oracle b/tests/ppwp/oracle/z.res.oracle index 36b867051bc631f062ee3acabac8d98edc0d1e57..fbc8797c38e03de54890cabd9c7f985afe9c7af9 100644 --- a/tests/ppwp/oracle/z.res.oracle +++ b/tests/ppwp/oracle/z.res.oracle @@ -4,7 +4,6 @@ Now output intermediate result [wp] Warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Qed] Goal typed_Z1m_ensures : Valid -[wp] [Cache] not used [wp] Proved goals: 1 / 1 Qed: 1 /* Generated by Frama-C */