diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 220f595078371d39769ca279359877beb0db5dde..cdb006d3a1eac09c041814a24b0eb0824699c34f 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -408,10 +408,8 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
         { spec_behavior = snd (List.split old_behaviors);
           spec_complete_behaviors = snd (List.split old_complete);
           spec_disjoint_behaviors = snd (List.split old_disjoint);
-          spec_terminates =
-            (Option.map snd) old_terminates;
-          spec_variant =
-            (Option.map snd) old_decreases
+          spec_terminates = Option.map snd old_terminates;
+          spec_variant = Option.map snd old_decreases
         }
       in
       let res = self#vspec spec in
@@ -430,6 +428,10 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
                b')
             old_behaviors
         in
+        Queue.add
+          (fun () ->
+             ignore (Annotations.funspec ~populate:false new_kf))
+          self#get_filling_actions ;
         let new_terminates =
           Option.map
             (fun (e,t) ->
diff --git a/tests/spec/non_ast_spec_copy.i b/tests/spec/non_ast_spec_copy.i
new file mode 100644
index 0000000000000000000000000000000000000000..6b0ef4c550a412730efd94394f932dc39a5ae550
--- /dev/null
+++ b/tests/spec/non_ast_spec_copy.i
@@ -0,0 +1,9 @@
+/* run.config
+   MODULE: @PTEST_NAME@
+   OPT: -copy
+*/
+
+// to be populated by non_ast_spec_copy.ml
+void function(void){
+
+}
diff --git a/tests/spec/non_ast_spec_copy.ml b/tests/spec/non_ast_spec_copy.ml
new file mode 100644
index 0000000000000000000000000000000000000000..03faef2019ec0970de6c518e0e11b08d5f5a7782
--- /dev/null
+++ b/tests/spec/non_ast_spec_copy.ml
@@ -0,0 +1,14 @@
+let add_terminates_true _ =
+  let terminates pred_loc =
+    Logic_const.(new_predicate { ptrue with pred_loc })
+  in
+  let add_terminates kf =
+    if Annotations.terminates ~populate:false kf = None then
+      Annotations.add_terminates
+        Emitter.kernel kf (terminates @@ Kernel_function.get_location kf)
+  in
+  Globals.Functions.iter add_terminates
+
+let () =
+  let category = File.register_code_transformation_category "my_category" in
+  File.add_code_transformation_after_cleanup category add_terminates_true
diff --git a/tests/spec/oracle/non_ast_spec_copy.res.oracle b/tests/spec/oracle/non_ast_spec_copy.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cefe9a19bcba0578e852a9f6baceca22f1bf4fef
--- /dev/null
+++ b/tests/spec/oracle/non_ast_spec_copy.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/spec/non_ast_spec_copy.i (no preprocessing)