diff --git a/master_changes.md b/master_changes.md
index 055f1684657..6d3b2cfd2a6 100644
--- a/master_changes.md
+++ b/master_changes.md
@@ -130,6 +130,7 @@ users)
 ## Solver
   * [BUG] Remove z3 debug output [#4723 @rjbou - fix #4717] [2.1.0~rc2 #4720]
   * Fix and improve the Z3 solver backend [#4880 @altgr]
+  * Refactored, fixed, improved and optimised the z3 solver backend [#4878 @altgr]
 
 ## Client
   *
diff --git a/src/core/opamConsole.ml b/src/core/opamConsole.ml
index c8eb45d2746..72a7cac20b8 100644
--- a/src/core/opamConsole.ml
+++ b/src/core/opamConsole.ml
@@ -506,12 +506,9 @@ let print_message =
 
 let timestamp () =
   let time = Unix.gettimeofday () -. global_start_time in
-  let tm = Unix.gmtime time in
-  let msec = time -. (floor time) in
-  Printf.ksprintf (colorise `blue) "%.2d:%.2d.%.3d"
-    (tm.Unix.tm_hour * 60 + tm.Unix.tm_min)
-    tm.Unix.tm_sec
-    (int_of_float (1000.0 *. msec))
+  Printf.ksprintf (colorise `blue) "%02.0f:%06.3f"
+    (time /. 60.)
+    (mod_float time 60.)
 
 let log_formatter, finalise_output =
   if Sys.win32 then
diff --git a/src/solver/opamBuiltinZ3.real.ml b/src/solver/opamBuiltinZ3.real.ml
index 38d2fb70d68..f85576d1496 100644
--- a/src/solver/opamBuiltinZ3.real.ml
+++ b/src/solver/opamBuiltinZ3.real.ml
@@ -41,46 +41,79 @@ let default_criteria = {
   crit_best_effort_prefix = Some "+count[opam-query,solution],";
 }
 
-let mk_or ctx = function
-  | None -> None
-  | Some [] -> None
-  | Some [p] -> Some p
-  | Some l -> Some (Z3.Boolean.mk_or ctx l)
+let ( @^ ) x l =
+  match Z3.Boolean.get_bool_value x with
+  | Z3enums.L_TRUE -> l
+  | Z3enums.L_FALSE -> [x]
+  | Z3enums.L_UNDEF -> match l with
+    | y :: _ when Z3.Expr.equal x y -> l
+    | _ -> x :: l
 
-let mk_and ctx = function
-  | None -> None
-  | Some [] -> None
-  | Some [p] -> Some p
-  | Some l -> Some (Z3.Boolean.mk_and ctx l)
+let (@@^) l1 l2 = match l1, l2 with
+  | [x], l | l, [x] ->
+    (match Z3.Boolean.get_bool_value x with
+     | Z3enums.L_TRUE -> l
+     | Z3enums.L_FALSE -> [x]
+     | Z3enums.L_UNDEF -> List.rev_append l1 l2)
+  | _ -> List.rev_append l1 l2
 
-let ( @^ ) opt l = match opt with
-  | None -> l
-  | Some x -> x :: l
+(* Mutable Z3 context expanded with generation intermediate information *)
+type ctx = {
+  z3: Z3.context;
+  pkgs: (Cudf.package, Z3.Expr.expr) Hashtbl.t;
+  constrs: (Cudf_types.vpkglist list, Z3.Expr.expr) Hashtbl.t;
+  mutable constr_defs: Z3.Expr.expr list;
+}
 
-let (@@^) o l = match o with
-  | None -> l
-  | Some l1 -> List.rev_append l1 l
+let mk_or ctx l =
+  if List.exists Z3.Boolean.is_true l then
+    Z3.Boolean.mk_true ctx.z3
+  else match List.filter OpamStd.Op.(not @* Z3.Boolean.is_false) l with
+    | [] -> Z3.Boolean.mk_false ctx.z3
+    | [p] -> p
+    | l -> Z3.Boolean.mk_or ctx.z3 l
 
-let xrmap f l =
-  match List.fold_left (fun acc x -> f x @^ acc) [] l with
-  | [] -> None
-  | l -> Some l
+let mk_and ctx l =
+  if List.exists Z3.Boolean.is_false l then
+    Z3.Boolean.mk_false ctx.z3
+  else match List.filter OpamStd.Op.(not @* Z3.Boolean.is_true) l with
+  | [] -> Z3.Boolean.mk_true ctx.z3
+  | [p] -> p
+  | l -> Z3.Boolean.mk_and ctx.z3 l
 
-(*
-let xmap f l = match xrmap f l with
-  | Some l -> Some (List.rev l)
-  | None -> None
-*)
-open OpamStd.Option.Op
+let mk_not ctx e =
+  if Z3.Boolean.is_true e then Z3.Boolean.mk_false ctx.z3
+  else if Z3.Boolean.is_false e then Z3.Boolean.mk_true ctx.z3
+  else Z3.Boolean.mk_not ctx.z3 e
+
+let psym ctx = Hashtbl.find ctx.pkgs
+
+let mk_constr ctx vpkgll pkgs =
+  let vpkgll = List.rev_map (List.sort compare) vpkgll in
+  let vpkgll = List.sort compare vpkgll in
+  try Hashtbl.find ctx.constrs vpkgll with Not_found ->
+    let c = mk_or ctx (List.map (psym ctx) pkgs) in
+    match Z3.Boolean.get_bool_value c, pkgs with
+    | Z3enums.L_UNDEF, (_::_::_::_) ->
+      let id =
+        Z3.Boolean.mk_const_s ctx.z3
+          (OpamStd.List.concat_map " & "
+             Cudf_types_pp.string_of_vpkglist vpkgll)
+      in
+      ctx.constr_defs <- Z3.Boolean.mk_eq ctx.z3 id c :: ctx.constr_defs;
+      Hashtbl.add ctx.constrs vpkgll id;
+      id
+    | _ -> c
+
+let expand_constraint universe ctx (name, constr) =
+  let pkgs = Cudf.lookup_packages universe ~filter:constr name in
+  mk_constr ctx [[name, constr]] pkgs
 
 let def_packages ctx (_preamble, universe, _request) =
-  let syms = Hashtbl.create 2731 in
-  let psym p = Hashtbl.find_opt syms p in
-  let psym_exn p = match psym p with None -> raise Not_found | Some p -> p in
   (* variable definitions *)
   Cudf.iter_packages (fun pkg ->
-      Hashtbl.add syms pkg
-        (Z3.Boolean.mk_const_s ctx
+      Hashtbl.add ctx.pkgs pkg
+        (Z3.Boolean.mk_const_s ctx.z3
            (Printf.sprintf "%s.%d" pkg.Cudf.package pkg.Cudf.version)))
     universe;
   let def_exprs = [] in
@@ -89,22 +122,19 @@ let def_packages ctx (_preamble, universe, _request) =
     Cudf.fold_packages_by_name (fun e _name pkgs ->
         let keep =
           match List.find (fun p -> p.Cudf.keep = `Keep_version) pkgs with
-          | p -> psym p
+          | p -> psym ctx p
           | exception Not_found ->
             if List.exists (fun p -> p.Cudf.keep = `Keep_package) pkgs then
-              mk_or ctx @@ xrmap psym pkgs
-            else None
+              mk_or ctx @@ List.map (psym ctx) pkgs
+            else
+              Z3.Boolean.mk_true ctx.z3
         in
         keep @^ e)
       def_exprs
       universe
   in
-  let expand_constraint pkg (name, constr) =
-    mk_or ctx
-      (xrmap (fun p -> if Cudf.( =% ) pkg p then None else psym p)
-         (Cudf.lookup_packages universe ~filter:constr name))
-  in
   let def_exprs =
+    (* depends, (ext) conflicts *)
     Cudf.fold_packages (fun e pkg ->
         let module SM = OpamStd.String.Map in
         let cudf_depends, cudf_depends_map =
@@ -117,146 +147,183 @@ let def_packages ctx (_preamble, universe, _request) =
             pkg.Cudf.depends
         in
         let depends =
-          xrmap
-            (fun disj -> mk_or ctx @@ xrmap (expand_constraint pkg) disj)
-            cudf_depends @@^
           SM.fold (fun name conj e ->
               (match
-                 xrmap psym @@
                  List.fold_left (fun plist disj ->
-                     let r =
-                       List.filter (fun p ->
-                           List.exists
-                             (fun (_, cstr) ->
-                                Cudf.version_matches p.Cudf.version cstr)
-                             disj)
-                         plist
-                     in
-                     r)
+                     List.filter (fun p ->
+                         List.exists
+                           (fun (_, cstr) ->
+                              Cudf.version_matches p.Cudf.version cstr)
+                           disj)
+                       plist)
                    (Cudf.lookup_packages universe name)
                    conj
                with
-               | None -> Some (Z3.Boolean.mk_false ctx)
-               | some -> mk_or ctx some)
+               | [] -> Z3.Boolean.mk_false ctx.z3
+               | pkgs -> mk_constr ctx conj pkgs)
               @^ e)
             cudf_depends_map
+          @@
+          List.fold_left
+            (fun e disj ->
+               (mk_or ctx @@ List.rev_map (expand_constraint universe ctx) disj)
+               @^ e)
             []
-          |> OpamStd.Option.some
-          |> mk_and ctx
-          >>| Z3.Boolean.mk_implies ctx (psym_exn pkg)
+            cudf_depends
         in
         let conflicts =
-          mk_or ctx @@ xrmap
-             (expand_constraint pkg)
-             pkg.Cudf.conflicts
-          >>| fun c ->
-          Z3.Boolean.mk_implies ctx (psym_exn pkg) (Z3.Boolean.mk_not ctx c)
+          let conflicts =
+            List.filter (fun cs -> cs <> (pkg.Cudf.package, None))
+              pkg.Cudf.conflicts
+          in
+          mk_not ctx @@ mk_or ctx @@ List.rev_map
+            (fun (name, filter) ->
+               let pkgs = Cudf.lookup_packages universe ~filter name in
+               if List.mem pkg pkgs then (* Avoid self-conflict *)
+                 mk_constr ctx
+                   [ [name, filter]; [name, Some (`Neq, pkg.Cudf.version)] ]
+                   (List.filter (fun p -> not (Cudf.( =% ) pkg p)) pkgs)
+               else
+                 mk_constr ctx[[name, filter]] pkgs)
+            conflicts
         in
-        depends @^ conflicts @^ e)
+        let cft_deps =
+          Z3.Boolean.mk_implies ctx.z3
+            (psym ctx pkg)
+            (mk_and ctx (conflicts @^ depends))
+        in
+        cft_deps @^ e)
       def_exprs
       universe
   in
-  List.rev def_exprs,
-  psym
-
-let def_request ctx (_preamble, universe, request) psym =
-  let expand_constraint (name, constr) =
-    mk_or ctx @@ xrmap psym
-      (Cudf.lookup_packages universe ~filter:constr name)
+  let def_exprs =
+    (* self-conflicts *)
+    Cudf.fold_packages_by_name (fun e name pkgs ->
+        let zero = Z3.Arithmetic.Integer.mk_numeral_i ctx.z3 0 in
+        let one = Z3.Arithmetic.Integer.mk_numeral_i ctx.z3 1 in
+        let cft_pkgs =
+          List.filter (fun p -> List.mem (name, None) p.Cudf.conflicts) pkgs
+        in
+        if List.length cft_pkgs >= 2 then
+          Z3.Boolean.mk_implies ctx.z3
+            (mk_constr ctx [[name, None]] pkgs)
+            (Z3.Arithmetic.mk_ge ctx.z3 one
+               (Z3.Arithmetic.mk_add ctx.z3
+                  (List.map
+                     (fun p -> Z3.Boolean.mk_ite ctx.z3 (psym ctx p) one zero)
+                     cft_pkgs)))
+          :: e
+        else e)
+      def_exprs
+      universe
   in
+  List.rev def_exprs
+
+let def_request ctx (_preamble, universe, request) =
   let inst =
-    xrmap expand_constraint request.Cudf.install
+    List.rev_map (expand_constraint universe ctx) request.Cudf.install
   in
   let rem =
-    xrmap
-      (fun vpkg -> expand_constraint vpkg >>| Z3.Boolean.mk_not ctx)
+    List.rev_map (fun vpkg -> mk_not ctx (expand_constraint universe ctx vpkg))
       request.Cudf.remove
   in
   let up =
-    xrmap (fun (name, constr) ->
+    List.rev_map (fun (name, constr) ->
         match Cudf.get_installed universe name with
         | [] ->
-          mk_or ctx @@ xrmap psym
+          mk_or ctx @@ List.rev_map (psym ctx)
             (Cudf.lookup_packages universe ~filter:constr name)
         | p::l ->
           let vmin =
-            List.fold_left (fun vmin p -> max vmin p.Cudf.version) p.Cudf.version l
+            List.fold_left (fun vmin p -> max vmin p.Cudf.version)
+              p.Cudf.version l
           in
-          Cudf.lookup_packages universe ~filter:constr name |>
-          List.filter (fun p -> p.Cudf.version >= vmin) |>
-          xrmap psym |>
           (* fixme: the spec states that an 'upgrade' request should guarantee
              that only one version of the package will be installed. Since it's
              already a constraint in opam, and it's non trivial to encode, we
              ignore it here. *)
-          mk_or ctx)
+          mk_or ctx @@ List.rev_map (psym ctx) @@
+          List.filter (fun p -> p.Cudf.version >= vmin) @@
+          Cudf.lookup_packages universe ~filter:constr name)
       request.Cudf.upgrade
   in
   inst @@^ rem @@^ up @@^ []
 
 let sum ctx (_, universe, _) filter value =
-  let ite filt iftrue iffalse =
-    Z3.Boolean.mk_ite ctx filt
-      (Z3.Arithmetic.Integer.mk_numeral_i ctx iftrue)
-      (Z3.Arithmetic.Integer.mk_numeral_i ctx iffalse)
+  let ite filt iftrue iffalse e =
+    match Z3.Boolean.get_bool_value filt with
+    | Z3enums.L_UNDEF ->
+      Z3.Boolean.mk_ite ctx.z3 filt
+        (Z3.Arithmetic.Integer.mk_numeral_i ctx.z3 iftrue)
+        (Z3.Arithmetic.Integer.mk_numeral_i ctx.z3 iffalse)
+      :: e
+    | _ -> e (* constants don't matter *)
   in
   Cudf.fold_packages (fun e pkg ->
-      match filter pkg with
-      | None -> e
-      | Some filt ->
-        match value pkg with
-        | 0 -> e
-        | n ->
-          if Z3.Boolean.is_not filt then
-            match Z3.Expr.get_args filt with
-            | [filt] -> ite filt 0 n :: e
-            | _ -> assert false
-          else
-            ite filt n 0 :: e)
+      match value pkg with
+      | 0 -> e
+      | n ->
+        let filt = filter pkg in
+        if Z3.Boolean.is_not filt then
+          match Z3.Expr.get_args filt with
+          | [filt] -> ite filt 0 n e
+          | _ -> assert false
+        else
+          ite filt n 0 e)
     []
     universe
 
-type filter = Installed | Changed | Removed | New | Upgraded | Downgraded | Requested
+type filter = Installed | Changed | Removed | New |
+              Upgraded | Downgraded | Requested
 type property = string option
 type sign = Plus | Minus
 
 type criterion = sign * filter * property
 
-let def_criterion ctx opt (preamble, universe, request as cudf) psym
+let def_criterion ctx opt (preamble, universe, request as cudf)
     (sign, filter, property : criterion) =
   let filter_f = match filter with
-    | Installed -> fun p -> psym p
+    | Installed -> fun p -> psym ctx p
     | Changed ->
       fun p ->
-        if p.Cudf.installed then psym p >>| Z3.Boolean.mk_not ctx
-        else psym p
+        if p.Cudf.installed then
+          (* true on both the removed version and the new version, if any,
+             according to the spec *)
+          mk_or ctx @@
+          (mk_not ctx (psym ctx p) ::
+           (List.rev_map (psym ctx)
+              (Cudf.lookup_packages universe p.Cudf.package
+                 ~filter:(Some (`Neq, p.Cudf.version)))))
+        else psym ctx p
     | Removed ->
       fun p ->
         if p.Cudf.installed then
-          mk_or ctx @@ xrmap psym (Cudf.lookup_packages universe p.Cudf.package)
-          >>| Z3.Boolean.mk_not ctx
-        else None
+          mk_not ctx @@ mk_or ctx @@
+          List.rev_map (psym ctx)
+            (Cudf.lookup_packages universe p.Cudf.package)
+        else Z3.Boolean.mk_false ctx.z3
     | New ->
       fun p ->
-        if p.Cudf.installed then None
+        if p.Cudf.installed then Z3.Boolean.mk_false ctx.z3
         else
-          mk_or ctx @@ xrmap psym (Cudf.lookup_packages universe p.Cudf.package)
+          mk_or ctx @@ List.rev_map (psym ctx)
+            (Cudf.lookup_packages universe p.Cudf.package)
     | Upgraded ->
       fun p ->
-        if p.Cudf.installed then None
-        else (match Cudf.get_installed universe p.Cudf.package with
-            | [] -> None
-            | l when List.for_all (fun p1 -> p1.Cudf.version < p.Cudf.version) l
-              -> psym p
-            | _ -> None)
+        if p.Cudf.installed then Z3.Boolean.mk_false ctx.z3
+        else if
+          List.for_all (fun p1 -> p1.Cudf.version < p.Cudf.version)
+            (Cudf.get_installed universe p.Cudf.package)
+        then psym ctx p
+        else Z3.Boolean.mk_false ctx.z3
     | Downgraded ->
       fun p ->
-        if p.Cudf.installed then None
-        else (match Cudf.get_installed universe p.Cudf.package with
-            | [] -> None
-            | l when List.exists (fun p1 -> p1.Cudf.version > p.Cudf.version) l
-              -> psym p
-            | _ -> None)
+        if p.Cudf.installed then Z3.Boolean.mk_false ctx.z3
+        else if
+          List.exists (fun p1 -> p1.Cudf.version > p.Cudf.version)
+            (Cudf.get_installed universe p.Cudf.package)
+        then psym ctx p
+        else Z3.Boolean.mk_false ctx.z3
     | Requested ->
       fun p ->
         if
@@ -266,8 +333,8 @@ let def_criterion ctx opt (preamble, universe, request as cudf) psym
           List.exists (fun (name, cstr) ->
               p.Cudf.package = name && Cudf.version_matches p.Cudf.version cstr)
             request.Cudf.upgrade
-        then psym p
-        else None
+        then psym ctx p
+        else Z3.Boolean.mk_false ctx.z3
   in
   let value_f = match property with
     | None -> fun _ -> 1
@@ -287,16 +354,17 @@ let def_criterion ctx opt (preamble, universe, request as cudf) psym
           | exception Not_found ->
             failwith ("Undefined CUDF property: "^prop)
   in
-  match sum ctx cudf filter_f value_f with
-  | [] -> None
-  | sum ->
-    OpamStd.Option.some @@
-    (match sign with Plus -> Z3.Optimize.maximize | Minus -> Z3.Optimize.minimize)
-      opt
-      (Z3.Arithmetic.mk_add ctx sum)
+  let tot = sum ctx cudf filter_f value_f in
+  if tot <> [] then
+    let optfun = match sign with
+      | Plus -> Z3.Optimize.maximize
+      | Minus -> Z3.Optimize.minimize
+    in
+    let _handle = optfun opt (Z3.Arithmetic.mk_add ctx.z3 tot) in
+    ()
 
-let def_criteria ctx opt cudf psym crits =
-  List.map (def_criterion ctx opt cudf psym) crits
+let def_criteria ctx opt cudf crits =
+  List.iter (def_criterion ctx opt cudf) crits
 
 module Syntax = struct
 
@@ -403,18 +471,42 @@ let call ~criteria ?timeout (preamble, universe, _ as cudf) =
     | None -> []
     | Some secs -> ["timeout", string_of_int (int_of_float (1000. *. secs))]
   in
-  let ctx = Z3.mk_context cfg in
-  let opt = Z3.Optimize.mk_opt ctx in
+  let ctx = {
+    z3 = Z3.mk_context cfg;
+    pkgs = Hashtbl.create 2731;
+    constrs = Hashtbl.create 2731;
+    constr_defs = [];
+  } in
   log "Generating package definitions";
-  let expr, psym = def_packages ctx cudf in
-  Z3.Optimize.add opt expr;
+  let packages_defs = def_packages ctx cudf in
   log "Generating request";
-  Z3.Optimize.add opt (def_request ctx cudf psym);
+  let request_def = def_request ctx cudf in
   log "Generating optimization criteria";
-  let _objs =
-    def_criteria ctx opt cudf psym (Syntax.criteria_of_string criteria)
+  let opt = Z3.Optimize.mk_opt ctx.z3 in
+  let _criteria_def_handles =
+    def_criteria ctx opt cudf (Syntax.criteria_of_string criteria)
+  in
+  log "Sending the problem to Z3";
+  let params =
+    Z3.Params.mk_params ctx.z3
+    (* |> (fun p -> Z3.Params.add_symbol p
+     *        (Z3.Symbol.mk_string ctx "priority")
+     *        (Z3.Symbol.mk_string ctx "box"); p) *)
+    (* |> (fun p -> Z3.Params.add_symbol p
+     *        (Z3.Symbol.mk_string ctx "maxsat_engine")
+     *        (Z3.Symbol.mk_string ctx "wmax"); p) *)
   in
+  Z3.Optimize.set_parameters opt params;
+  Z3.Optimize.add opt packages_defs;
+  Z3.Optimize.add opt ctx.constr_defs;
+  Z3.Optimize.add opt request_def;
   log "Resolving...";
+  (* (match Sys.getenv "OPAMZ3DEBUG" with
+   *  | exception Not_found -> ()
+   *  | f ->
+   *    let debug = open_out (f^".smt2") in
+   *    output_string debug (Z3.Optimize.to_string opt);
+   *    close_out debug); *)
   match Z3.Optimize.check opt with
   | UNSATISFIABLE ->
     log "UNSAT";
diff --git a/src/solver/opamCudf.ml b/src/solver/opamCudf.ml
index 622d23b6989..22cd7442ab8 100644
--- a/src/solver/opamCudf.ml
+++ b/src/solver/opamCudf.ml
@@ -1363,17 +1363,18 @@ let call_external_solver ~version_map univ req =
       let msg =
         Printf.sprintf
           "Solver failure: %s\nThis may be due to bad settings (solver or \
-           solver criteria) or a broken solver solver installation. Check \
+           solver criteria) or a broken solver installation. Check \
            $OPAMROOT/config, and the --solver and --criteria options."
           msg
       in
       raise (Solver_failure msg)
     | e ->
       OpamStd.Exn.fatal e;
+      let bt = Printexc.get_raw_backtrace () in
       let msg =
         Printf.sprintf "Solver failed: %s" (Printexc.to_string e)
       in
-      raise (Solver_failure msg)
+      Printexc.raise_with_backtrace (Solver_failure msg) bt
   else
     Dose_algo.Depsolver.Sat(None,Cudf.load_universe [])
 
diff --git a/src/solver/opamSolver.ml b/src/solver/opamSolver.ml
index 96b9fe130e0..846af297fd7 100644
--- a/src/solver/opamSolver.ml
+++ b/src/solver/opamSolver.ml
@@ -453,7 +453,11 @@ let resolve universe ~orphans request =
         (invariant_pkg.Cudf.package, invariant_pkg.Cudf.version);
       OpamCudf.to_actions add_orphan_packages u resp
     with OpamCudf.Solver_failure msg ->
-      OpamConsole.error_and_exit `Solver_failure "%s" msg
+      let bt = Printexc.get_raw_backtrace () in
+      OpamConsole.error "%s" msg;
+      Printexc.raise_with_backtrace
+        OpamStd.Sys.(Exit (get_exit_code `Solver_failure))
+        bt
   in
   match resolve simple_universe cudf_request with
   | Conflicts _ as c -> c
diff --git a/src/solver/opamSolverConfig.ml b/src/solver/opamSolverConfig.ml
index 7d0d303ed8e..1a2426b8742 100644
--- a/src/solver/opamSolverConfig.ml
+++ b/src/solver/opamSolverConfig.ml
@@ -250,4 +250,7 @@ let call_solver ~criteria cudf =
   let module S = (val Lazy.force (!r.solver)) in
   OpamConsole.log "SOLVER" "Calling solver %s with criteria %s"
     (OpamCudfSolver.get_name (module S)) criteria;
-  S.call ~criteria ?timeout:(!r.solver_timeout) cudf
+  let chrono = OpamConsole.timer () in
+  let r = S.call ~criteria ?timeout:(!r.solver_timeout) cudf in
+  OpamConsole.log "SOLVER" "External solver took %.3fs" (chrono ());
+  r