diff --git a/src/kernel_internals/typing/allocates.ml b/src/kernel_internals/typing/allocates.ml
index 7b732f4edf83cefc6aa9e672b86c541c014648b6..21d04239663de36f3e20c3b6e81bc6a4e9a292be 100644
--- a/src/kernel_internals/typing/allocates.ml
+++ b/src/kernel_internals/typing/allocates.ml
@@ -35,7 +35,7 @@ let add_allocates_loop stmt =
   let all_default = Annotations.fold_code_annot all_default stmt true in
   if all_default then
     let ca = AAllocation ([], FreeAlloc ([], [])) in
-    Annotations.add_code_annot Emitter.kernel stmt
+    Annotations.add_code_annot ~keep_empty:false Emitter.kernel stmt
       (Logic_const.new_code_annotation ca)
 
 let add_allocates_nothing_funspec kf =
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 004941db6742cd482c8910fc0e7a1d3f3d0f197a..7ce63778b530c98bf41e20013662ec11946bf0c9 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -272,7 +272,10 @@ let update_loop_assigns kf stmt state vi code_annot =
         (AAssigns (bhvs, Logic_utils.concat_assigns old_assigns assigns))
     | _ -> Aorai_option.fatal "Expecting an assigns clause here"
   in
-  Annotations.add_code_annot Aorai_option.emitter ~kf stmt new_assigns
+  (* we're putting the annotation on a new statement, with an empty
+     loop assigns by construction. Don't keep_empty *)
+  Annotations.add_code_annot
+    ~keep_empty:false Aorai_option.emitter ~kf stmt new_assigns
 
 let get_action_post_cond kf ?init_trans return_states =
   let to_consider pre_state int_states =