diff --git a/dev/build-release.sh b/dev/build-release.sh
index b1298e62f590fea679edb5fbd9cd95a499b4ed4d..424a9a77e632a14c39e1efda2f9ddc4107f42ec1 100755
--- a/dev/build-release.sh
+++ b/dev/build-release.sh
@@ -95,12 +95,14 @@ VERSION_AND_CODENAME="${VERSION_SAFE}-${CODENAME}"
 if [ "$VERSION_MINOR" != 0 ]; then
   # We compare new minor to previous minor
   PREVIOUS="$VERSION_MAJOR.$((VERSION_MINOR - 1))"
+  PREVIOUS_TAG="$PREVIOUS"
 else
   # We compare new major to previous major, the exact previous version is not
   # of interest for a new major version
   PREVIOUS="$((VERSION_MAJOR - 1))"
+  PREVIOUS_TAG="$PREVIOUS.0"
 fi
-PREVIOUS_NAME=$(git show $PREVIOUS:VERSION_CODENAME)
+PREVIOUS_NAME=$(git show "$PREVIOUS_TAG":VERSION_CODENAME)
 
 if [ "$VERSION_MODIFIER" == "+dev" ]; then
   echo "Development version ($VERSION)"
diff --git a/ivette/package.json b/ivette/package.json
index 963ec0dee1974fcb9c453bf166c2ee1f23d5d4a0..5c7f570893ed8f47c798c6d588beb36ca1274f06 100644
--- a/ivette/package.json
+++ b/ivette/package.json
@@ -1,7 +1,7 @@
 {
   "name": "ivette",
   "productName": "Ivette",
-  "version": "1.0.0",
+  "version": "28.0.0",
   "main": "index.js",
   "repository": "git@git.frama-c.com:frama-c/Ivette.git",
   "author": "Loïc Correnson <loic.correnson@cea.fr>",
diff --git a/ivette/src/dome/template/makefile b/ivette/src/dome/template/makefile
index 6318b5d6827bacda0fd474b003d00b90f0fa1445..9696ab4c617429307a8e8bc18ff13e5bfbff0db6 100644
--- a/ivette/src/dome/template/makefile
+++ b/ivette/src/dome/template/makefile
@@ -270,7 +270,7 @@ dome-dist-win: dome-app
 
 dome-dist-mac: dome-app
 	@echo "[Dome] packaging application (macOS exe)"
-	DOME=$(DOME) yarn run electron-builder --mac
+	DOME=$(DOME) yarn run electron-builder --mac -c.mac.identity=null
 	@echo "[Dome] application packaged in ./dist"
 
 # --------------------------------------------------------------------------
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index 2a958392965192ef88c06af011782957f59be145..068faf90639e77bfab3b14a73f96c956dd044db0 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -62,16 +62,24 @@ let configure =
 
 type t = Why3.Whyconf.prover
 
+(* In an ambiguous map of provers, tries to find the basic alternative, if none
+   is found, just give an arbitrary one. *)
+let resolve_ambiguity provers =
+  let open Why3.Whyconf in
+  let provers = fst @@ List.split @@ Mprover.bindings provers in
+  try List.find (fun p -> p.prover_altern = "") provers
+  with Not_found -> List.hd provers
+
 let find_opt s =
+  let open Why3.Whyconf in
   try
     let config = Lazy.force cfg in
-    let filter = Why3.Whyconf.parse_filter_prover s in
-    Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
+    let filter = parse_filter_prover s in
+    Some ((filter_one_prover config filter).prover)
   with
-  | Why3.Whyconf.ProverNotFound _
-  | Why3.Whyconf.ParseFilterProver _
-  | Why3.Whyconf.ProverAmbiguity _  ->
-    None
+  | ParseFilterProver _ -> None
+  | ProverNotFound _ -> None
+  | ProverAmbiguity (_, _, provers)  -> Some (resolve_ambiguity provers)
 
 type fallback = Exact of t | Fallback of t | NotFound
 
@@ -79,18 +87,14 @@ let find_fallback name =
   match find_opt name with
   | Some prv -> Exact prv
   | None ->
-    (* Why3 should deal with this intermediate case *)
-    match find_opt (String.lowercase_ascii name) with
-    | Some prv -> Exact prv
-    | None ->
-      match String.split_on_char ',' name with
-      | shortname :: _ :: _ ->
-        begin
-          match find_opt (String.lowercase_ascii shortname) with
-          | Some prv -> Fallback prv
-          | None -> NotFound
-        end
-      | _ -> NotFound
+    match String.split_on_char ',' name with
+    | shortname :: _ :: _ ->
+      begin
+        match find_opt (String.lowercase_ascii shortname) with
+        | Some prv -> Fallback prv
+        | None -> NotFound
+      end
+    | _ -> NotFound
 
 let ident_why3 = Why3.Whyconf.prover_parseable_format
 let ident_wp s =
diff --git a/src/plugins/wp/gui/GuiConfig.ml b/src/plugins/wp/gui/GuiConfig.ml
index a6ba232e23f2945dc795bb5c9fd3aff42c1ad2f2..f40609610d935c291e8d1bfe4e24c46efb05d3d7 100644
--- a/src/plugins/wp/gui/GuiConfig.ml
+++ b/src/plugins/wp/gui/GuiConfig.ml
@@ -36,7 +36,7 @@ class provers =
         (* select automatically the provers set on the command line *)
         let cmdline =
           match Wp_parameters.Provers.get () with
-          | [] -> [ "alt-ergo" ]
+          | [] -> [ "Alt-Ergo" ]
           | prvs -> prvs
         in
         let selection = List.fold_left
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 1823763111f162e7261f4cba82782fac30b490f9..aa5f216834730e120fd970205bda9514730b3d83 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -565,7 +565,7 @@ let spawn_wp_proofs ~script goals =
 
 let get_prover_names () =
   match Wp_parameters.Provers.get () with
-  | [] -> [ "alt-ergo" ] | pnames -> pnames
+  | [] -> [ "Alt-Ergo" ] | pnames -> pnames
 
 let compute_provers ~mode ~script =
   script.provers <- List.fold_right
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index 369d710cdd7fdf82a6d78fc37a061e96c2e195e5..891afaeb731f32e9760851a8b335438cf2f17072 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -22,7 +22,7 @@ let run () =
          | None -> prvs
          | Some VCS.Tactical -> prvs
          | Some prv -> (VCS.Batch, prv) :: prvs)
-      ["alt-ergo"] []
+      ["Alt-Ergo"] []
   in
 
   let spawn goal =