diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle
index 9b5a7ccd075f8933eb54a906db21a5ab0e1af3ff..75a043ab71e0d4b5392bd12ecf2d3fe42a05f8b8 100644
--- a/tests/bugs/oracle/term.res.oracle
+++ b/tests/bugs/oracle/term.res.oracle
@@ -2,10 +2,12 @@
 [kernel] Parsing tests/bugs/term.cpp (external front-end)
 Now output intermediate result
 [wp] Running WP plugin...
-[wp] tests/bugs/term.cpp:49: Warning: 
-  Ignored 'terminates' specification:
-   \true
 [wp] Warning: Missing RTE guards
+[wp] tests/bugs/term.cpp:11: Warning: Terminates not implemented yet (skipped).
+[wp] tests/bugs/term.cpp:17: Warning: Terminates not implemented yet (skipped).
+[wp] tests/bugs/term.cpp:43: Warning: Terminates not implemented yet (skipped).
+[wp] tests/bugs/term.cpp:26: Warning: Terminates not implemented yet (skipped).
+[wp] tests/bugs/term.cpp:34: Warning: Terminates not implemented yet (skipped).
 [wp] 3 goals scheduled
 [wp] [Qed] Goal typed_Z2m2_ensures : Valid
 [wp] [Qed] Goal typed_Z2m3_c_ensures : Valid