diff --git a/Changelog b/Changelog
index 356c0d9f00df51165f5a03714c12c180256bd2db..89126925807b1f70a5c6a1ac8265ecad0f82796d 100644
--- a/Changelog
+++ b/Changelog
@@ -17,6 +17,15 @@
 Open Source Release <next-release>
 ##################################
 
+-*  Kernel    [2019/08/20] Fixes a rare but critical bug which occured when
+              Frama-C internally switched the current project in presence of >2
+              projects and destroyed the old current project at about the same
+              time: the Frama-C internal state became inconsistent and lead to
+              unsound computations and crashes. It may be revealed to the
+              end-user when using a long sequence of -then-replace (at least 3
+              of them).
+-*  Kernel    [2019/08/20] Fixed sequence of -removed-projects and -then
+              options.
 o   Ptests    [2019/08/05] Add new MODULE directive for compiling and loading
               an auxiliary OCaml module for a test
 -   Kernel    [2019/08/05] Add -keep-unused-types normalization option
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 02f357e8ebbc52cf9fb7883e3551c04d322a9a6b..41dcb5d8d089e8d56b26ceba6a29e28d14e31de2 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1522,7 +1522,14 @@ let _ =
 
 let () =
   Cmdline.run_after_configuring_stage
-    (fun () -> Remove_projects.iter (fun project -> Project.remove ~project ()))
+    (fun () ->
+       (* clear "-remove-projects" before itering over (a copy of) its contents
+          in order to prevent warnings about dangling pointer deletion (since it
+          is itself projectified and so contains a pointer to the project being
+          removed). *)
+       let s = Remove_projects.get () in
+       Remove_projects.clear ();
+       Project.Datatype.Set.iter (fun project -> Project.remove ~project ()) s)
 
 (* ************************************************************************* *)
 (** {2 Others options} *)
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 55280721f01c32fbc314ed7bc74e1571363aae86..27ff62f432dcb24838c06800b3c6a07c4da9e4f8 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -361,6 +361,9 @@ let journalized_set_current =
 let set_current ?(on=false) ?(selection=State_selection.full) p =
   if not (equal p (current ())) then journalized_set_current on selection p
 
+let set_current_as_last_created () =
+  Extlib.may (fun p -> set_current p) !last_created_by_copy_ref
+
 (** Indicates if we should keep [p] as the current project when calling {!on p}. *)
 let keep_current: bool ref = ref false
 
@@ -376,12 +379,12 @@ let on ?selection p f x =
   if old_current == p then f x
   else
     let set p = set_current ~on:true ?selection p in
-    let set_to_old () =
+    let rec set_to_old old =
       if not !keep_current then
         try
           (* if someone asks for keeping [p] as current during the execution of
              [f], do not restore [old_current] at the end. *)
-          set old_current
+          set old
         with Invalid_argument _ ->
           (* the old current project has been remove: replace it by the previous
              one, if any *)
@@ -390,16 +393,16 @@ let on ?selection p f x =
               old_current.unique_name
               (current ()).unique_name
           else
-            Q.move_at_top (Q.nth 1 projects) projects
+            set_to_old (Q.nth 1 projects)
     in
     let go () =
       set p;
       let r = f x in
-      set_to_old ();
+      set_to_old old_current;
       r
     in
     if debug_atleast 1 then go ()
-    else begin try go () with e -> set_to_old (); raise e end
+    else begin try go () with e -> set_to_old old_current; raise e end
 
 (* [set_current] must never be called internally. *)
 module Hide_set_current = struct let set_current () = assert false end
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index d24b9b72f021aa85a77861a275c364da006b82cf..ec2f4d49c9be6e619e6cd6dc672ffe4a53f31c8e 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -142,6 +142,10 @@ val set_keep_current: bool -> unit
       of the current {!on}) iff [b] is [true].
       @since Aluminium-20160501 *)
 
+(**/**)
+val set_current_as_last_created: unit -> unit
+(**/**)
+
 val copy: ?selection:State_selection.t -> ?src:t -> t -> unit
   (** Copy a project into another one. Default project for [src] is [current
       ()]. Replace the destination by [src].
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index bb11d8d56877746f7cea5b12005396ff6ddbeaad..287a5d8e0b01a50e36a5dd37f0f4ea3ba4d3209f 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1863,7 +1863,9 @@ let toplevel play =
             Task.on_idle :=
               (fun f -> ignore (Glib.Timeout.add ~ms:50 ~callback:f));
             let project_name = Gui_parameters.Project_name.get () in
-            if project_name <> "" then
+            if project_name = "" then
+              Project.set_current_as_last_created ()
+            else
               Project.set_current (Project.from_unique_name project_name);
             Ast.compute ()
           with e -> (* An error occurred: we need to enforce the splash screen