[logic] fix some missing ~keep_empty:false

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 =

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 =