diff --git a/src/plugins/e-acsl/dup_functions.ml b/src/plugins/e-acsl/dup_functions.ml
index 40533cbe9b3965aa8408a8492a59c555bfe90c27..287b652d9baf8d489c00d507ad7b2c4326bf7577 100644
--- a/src/plugins/e-acsl/dup_functions.ml
+++ b/src/plugins/e-acsl/dup_functions.ml
@@ -92,8 +92,8 @@ let copy_ppt old_prj new_prj old_ppt new_ppt =
 (* ********************************************************************** *)
 
 let dup_spec_status old_prj kf new_kf old_spec new_spec =
-  let old_ppts = Property.ip_of_spec kf Kglobal old_spec in
-  let new_ppts = Property.ip_of_spec new_kf Kglobal new_spec in
+  let old_ppts = Property.ip_of_spec kf Kglobal ~active:[] old_spec in
+  let new_ppts = Property.ip_of_spec new_kf Kglobal ~active:[] new_spec in
   List.iter2 (copy_ppt old_prj (Project.current ())) old_ppts new_ppts
 
 let dup_funspec tbl bhv spec =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
index a74eb1cb0620527504a402e2dce7643c1286c1de..7b2aac32b7ae44a4c9a77e1b84860e8449e2ad1a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle
@@ -24,10 +24,10 @@ tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time
 tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid.
 tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown.
 tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time
-tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
+tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index f72e237a61fe41b778edd7e7df6564f34dd45b79..2c50b348cb869acef76cfb98b531837b375eeaf5 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -853,20 +853,20 @@ let translate_pre_spec kf kinstr env spec =
     | [] -> ()
     | l ->
       unsupported
-	(List.iter
-	   (fun l ->
-	     if must_translate (Property.ip_of_complete kf kinstr l) then
-	       not_yet env "complete behaviors"))
-	l);
+        (List.iter
+           (fun l ->
+             if must_translate (Property.ip_of_complete kf kinstr ~active:[] l)
+             then not_yet env "complete behaviors"))
+        l);
     (match spec.spec_disjoint_behaviors with
     | [] -> ()
     | l ->
       unsupported
-	(List.iter
-	   (fun l ->
-	     if must_translate (Property.ip_of_disjoint kf kinstr l) then
-	       not_yet env "disjoint behaviors"))
-	l);
+        (List.iter
+           (fun l ->
+             if must_translate (Property.ip_of_disjoint kf kinstr ~active:[] l)
+             then not_yet env "disjoint behaviors"))
+        l);
     env
   in
   let env = convert_unsupported_clauses env in