diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 959969454f5dc529b6b9a3b84eeaf984e2719532..4998c5f9d5074ab9de3ada998fc0e4fcca7b922a 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -277,6 +277,7 @@ module Normalized = struct
   type t = string
 
   let of_string ?existence ?base_name s = normalize ?existence ?base_name s
+  let extend ?existence t ext = normalize ?existence (t ^ ext)
   let concat ?existence t s = normalize ?existence (t ^ "/" ^ s)
   let concats ?existence t sl =
     let s' = List.fold_left (fun acc s -> acc ^ "/" ^ s) "" sl in
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index cdcaac29a4417a6e986fdda997693f2ebf787ce6..cb514384a962c603e1d6c8bb827d2fd912a5c2a7 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -74,6 +74,14 @@ module Normalized: sig
   *)
   val of_string: ?existence:existence -> ?base_name:string -> string -> t
 
+  (** [extend ~existence file ext] returns the normalized path to the file
+      [file] ^ [ext]. Note that it does not introduce a dot.
+      The resulting path must respect [existence].
+
+      @since Frama-C+dev
+  *)
+  val extend: ?existence:existence -> t -> string -> t
+
   (** [concat ~existence dir file] returns the normalized path
       resulting from the concatenation of [dir] ^ "/" ^ [file].
       The resulting path must respect [existence].
@@ -82,11 +90,10 @@ module Normalized: sig
   *)
   val concat: ?existence:existence -> t -> string -> t
 
-  (**
-     [concats ~existence dir paths] concatenates a list of paths, as per
-     the [concat] function.
+  (** [concats ~existence dir paths] concatenates a list of paths, as per
+      the [concat] function.
 
-     @since 28.0-Nickel
+      @since 28.0-Nickel
   *)
   val concats: ?existence:existence -> t -> string list -> t
 
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 62935c0fd4e636d0ee8a65008939ed3f235f1cc8..46700b024bbb668a92503d3782ea2aae1defc81f 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1413,10 +1413,11 @@ let editor_command pconf =
 
 let scriptfile ~force ~ext wpo =
   let dir = Wp_parameters.get_session_dir ~force "interactive" in
-  Filepath.Normalized.concat dir (wpo.Wpo.po_sid ^ ext)
+  let filenoext = Filepath.Normalized.concat dir wpo.Wpo.po_sid in
+  Filepath.Normalized.extend filenoext ext
 
 let updatescript ~script driver task =
-  let backup = Filepath.Normalized.concat script ".bak" in
+  let backup = Filepath.Normalized.extend script ".bak" in
   Filepath.rename script backup ;
   let old = open_in (backup :> string) in
   Command.pp_to_file script