diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 64f476c9d08467336e4e93104c7c03f1dae2a39f..e2b1dfa4cfbefc940b65b9eee34a1e5a110f1196 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1151,16 +1151,18 @@ let add_code_annot emitter ?kf stmt ca =
            "trying to register a second variant for statement %a"
            Stmt.pretty stmt)
     | AAssigns (bhvs, assigns) ->
-      let filter ca =
+      let filter_ca ca =
         match ca.annot_content with
         | AAssigns (bhvs', _) -> is_same_behavior_set bhvs bhvs'
         | _ -> false
       in
-      let ca' = code_annot ~filter stmt in
+      let filter e ca = Emitter.equal e emitter && filter_ca ca in
+      let ca_e = code_annot_emitter ~filter stmt in
+      let ca_total = code_annot ~filter:filter_ca stmt in
       let new_a =
-        match ca' with
+        match ca_e with
         | [] -> a
-        | [ { annot_content = AAssigns(_, assigns') } as ca ] ->
+        | [ { annot_content = AAssigns(_, assigns') } as ca,_ ] ->
           remove_code_annot_internal emitter ~kf stmt ca;
           let merged =
             merge_assigns ~keep_empty:false assigns' assigns
@@ -1171,7 +1173,18 @@ let add_code_annot emitter ?kf stmt ca =
             "More than one loop assigns clause for a statement. \
              Annotations internal state broken."
       in
-      let ips = Property.ip_of_code_annot kf stmt new_a in
+      let ips =
+        match ca_total with
+        | [] -> Property.ip_of_code_annot kf stmt a
+        | [ { annot_content = AAssigns (_,assigns') } ] ->
+          let merged = merge_assigns ~keep_empty:false assigns' assigns in
+          Property.ip_of_code_annot
+            kf stmt { a with annot_content = AAssigns(bhvs,merged) }
+        | _ ->
+          Kernel.fatal
+            "More than one loop assigns clause for a statement. \
+             Annotations internal state broken."
+      in
       new_a, ips
     | AAllocation (bhvs, alloc) ->
       let filter ca =
diff --git a/tests/spec/loop_assigns_generated.ml b/tests/spec/loop_assigns_generated.ml
index 7ac50e360b164722724652ddbf53dc1e19e182cc..c2c3d9d99bcfcd4f53e0aa41c51244450c9597ac 100644
--- a/tests/spec/loop_assigns_generated.ml
+++ b/tests/spec/loop_assigns_generated.ml
@@ -49,10 +49,12 @@ let main () =
   in
   let j = Cil.makeLocalVar def ~insert:true "j" Cil.intType in
   let k = Cil.makeLocalVar def ~insert:true "k" Cil.intType in
+  let l = Cil.makeLocalVar def ~insert:true "l" Cil.intType in
   let p = Cil.makeLocalVar def ~insert:true "p" Cil.intPtrType in
   let q = Cil.makeLocalVar def ~insert:true "q" Cil.intPtrType in
   add_assigns e1 kf s j;
   add_assigns e2 kf s k;
+  add_assigns e1 kf s l;
   add_allocates e1 kf s p;
   add_allocates e2 kf s q;
   Annotations.iter_code_annot (check_only_one Logic_utils.is_assigns) s;
diff --git a/tests/spec/oracle/loop_assigns_generated.res.oracle b/tests/spec/oracle/loop_assigns_generated.res.oracle
index b2a2c0e90847e95fdd62cf2ded3490d01d8b5c4e..6933252f4d1b9990d3d5f0406afc1e837bba74ca 100644
--- a/tests/spec/oracle/loop_assigns_generated.res.oracle
+++ b/tests/spec/oracle/loop_assigns_generated.res.oracle
@@ -4,10 +4,12 @@ void f(void)
 {
   int *q;
   int *p;
+  int l;
   int k;
   int j;
   int i = 0;
-  /*@ loop assigns i, (added_by_emitter1: j), (added_by_emitter2: k);
+  /*@ loop assigns i, (added_by_emitter1: j), (added_by_emitter1: l),
+                   (added_by_emitter2: k);
       loop allocates (added_by_emitter1: p), (added_by_emitter2: q);
   */
   while (i < 10) i ++;