diff --git a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
index d42e5c2b3412fdefaefe7a664138d210508157b5..4ec9f22c99e0e7620659bd5eee9ec60410685709 100644
--- a/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
+++ b/src/kernel_services/ast_transformations/inline_stmt_contracts.ml
@@ -65,10 +65,12 @@ class inline_stmt_contract =
          | [] -> Cil.DoChildren
          | _ ->
            let nop = Cil.mkStmtOneInstr ~valid_sid:true (Skip loc) in
-           List.iter (Annotations.add_code_annot emitter nop) posts;
+           let kf = Option.get self#current_kf in
+           List.iter (Annotations.add_code_annot emitter ~kf nop) posts;
            let b = Cil.mkBlockNonScoping [s; nop] in
            let b = Cil.transient_block b in
            let res = Cil.mkStmt ~valid_sid:true (Block b) in
+           Ast.mark_as_changed ();
            File.must_recompute_cfg (Option.get self#current_func);
            ChangeTo res
         )
diff --git a/tests/syntax/oracle/inline_stmt_contract.res.oracle b/tests/syntax/oracle/inline_stmt_contract.res.oracle
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..39a85c89c69eb63d2706ff0eeb968d2a5ee50f8c 100644
--- a/tests/syntax/oracle/inline_stmt_contract.res.oracle
+++ b/tests/syntax/oracle/inline_stmt_contract.res.oracle
@@ -0,0 +1,68 @@
+[kernel] Parsing inline_stmt_contract.i (no preprocessing)
+/* Generated by Frama-C */
+int X;
+int f(void)
+{
+  /*@ assert inline_stmt_contract: X ≡ 0; */
+  /*@ requires X ≡ 0;
+      ensures X ≡ 1; */
+  X ++;
+  /*@ assert inline_stmt_contract: X ≡ 1; */ ;
+  return X;
+}
+
+int g(void)
+{
+  __fc_inline_contract_label_0:
+  /*@ assert inline_stmt_contract: X ≥ 0 ⇒ X > -1; */
+  /*@ behavior b:
+        assumes X ≥ 0;
+        requires X > -1;
+        ensures X ≡ 0; */
+  if (X >= 0) X = 0; else X = -1;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≥ 0,__fc_inline_contract_label_0) ⇒ X ≡ 0;
+   */
+  ;
+  return X;
+}
+
+int h(void)
+{
+  int __retres;
+  /*@ ensures \false; */
+  {
+    __retres = 1;
+    goto return_label;
+  }
+  /*@ assert inline_stmt_contract: \false; */ ;
+  return_label: return __retres;
+}
+
+int i(void)
+{
+  __fc_inline_contract_label_0:
+  /*@ behavior b0:
+        assumes X ≡ 0;
+        ensures X ≡ 1; */
+  X ++;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≡ 0,__fc_inline_contract_label_0) ⇒ X ≡ 1;
+   */
+  ;
+  __fc_inline_contract_label_1:
+  /*@ behavior b1:
+        assumes X ≡ 1;
+        ensures X ≡ 2; */
+  X ++;
+  /*@
+  assert
+  inline_stmt_contract: \at(X ≡ 1,__fc_inline_contract_label_1) ⇒ X ≡ 2;
+   */
+  ;
+  return X;
+}
+
+