diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index 4668713a3706888b7b18bffd0ceb25d6e0d83df6..88365a5169fcfe938e308a6d176b9b69c5e473c5 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -44,6 +44,11 @@ let mark_unknown_requires kinstr kf funspec =
   in
   List.iter emit_behavior funspec.spec_behavior
 
+let need_assigns funspec =
+  match Cil.find_default_behavior funspec with
+  | None -> true
+  | Some bhv -> bhv.b_assigns = WritesAny
+
 let get_spec kinstr kf =
   let funspec = Annotations.funspec ~populate:false kf in
   if List.for_all (fun b -> b.b_assigns = WritesAny) funspec.spec_behavior
@@ -75,6 +80,15 @@ let get_spec kinstr kf =
         (if depth > 0 then Format.asprintf " of depth %i" depth else "")
         Kernel_function.pretty kf
     in
+    let funspec =
+      if need_assigns funspec
+      then
+        begin
+          ignore (!Annotations.populate_spec_ref kf funspec);
+          Annotations.funspec ~populate:false kf
+        end
+      else funspec
+    in
     mark_unknown_requires kinstr kf funspec;
     funspec