diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 78eed54a2d75a6a1b3af3d6f5dac7b5b62647bee..2fc2e6b4a4fab68b201fe30d18f9b3fbc6d8fecb 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -328,14 +328,15 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
     (fun p -> if WpPropId.filter_status p then WpAnnot.set_unreachable p)
     infos.doomed ;
   (* Trivial terminates *)
-  begin match CfgAnnot.get_terminates_goal kf with
-    | Some (id, _t)
-      when selected_terminates ~prop kf
-        && infos.calls = Fset.empty
-        && infos.no_variant_loops = Sset.empty ->
-        WpAnnot.set_trivially_terminates id
-    | _ -> ()
-  end ;
+  if Kernel_function.is_definition kf then
+    begin match CfgAnnot.get_terminates_goal kf with
+      | Some (id, _t)
+        when selected_terminates ~prop kf
+          && infos.calls = Fset.empty
+          && infos.no_variant_loops = Sset.empty ->
+          WpAnnot.set_trivially_terminates id
+      | _ -> ()
+    end ;
   (* Collected Infos *)
   infos