diff --git a/GillianCore/GIL_Syntax/BranchCase.ml b/GillianCore/GIL_Syntax/BranchCase.ml
deleted file mode 100644
index b3a3cf4cd..000000000
--- a/GillianCore/GIL_Syntax/BranchCase.ml
+++ /dev/null
@@ -1,9 +0,0 @@
-type t =
-  | GuardedGoto of bool
-  | LCmd of int
-  | SpecExec of Flag.t * int
-  | LAction of int
-  | LActionFail of int
-[@@deriving show, yojson]
-
-type path = t list [@@deriving yojson]
diff --git a/GillianCore/GIL_Syntax/Branch_case.ml b/GillianCore/GIL_Syntax/Branch_case.ml
new file mode 100644
index 000000000..4b169e55d
--- /dev/null
+++ b/GillianCore/GIL_Syntax/Branch_case.ml
@@ -0,0 +1,16 @@
+type t =
+  | GuardedGoto of bool
+  | LCmd of int
+  | SpecExec of Flag.t * int
+  | LAction of int
+  | LActionFail of int
+[@@deriving show, yojson]
+
+type path = t list [@@deriving yojson]
+
+let pp_short fmt = function
+  | GuardedGoto b -> Fmt.pf fmt "%B" b
+  | LCmd x -> Fmt.pf fmt "%d" x
+  | SpecExec (fl, i) -> Fmt.pf fmt "%a-%d" Flag.pp fl i
+  | LAction x -> Fmt.pf fmt "L%d" x
+  | LActionFail x -> Fmt.pf fmt "LF%d" x
diff --git a/GillianCore/GIL_Syntax/Gil_syntax.ml b/GillianCore/GIL_Syntax/Gil_syntax.ml
index 19d278431..8f646982b 100644
--- a/GillianCore/GIL_Syntax/Gil_syntax.ml
+++ b/GillianCore/GIL_Syntax/Gil_syntax.ml
@@ -3,7 +3,7 @@ module Annot = Annot
 module Asrt = Asrt
 module BinOp = BinOp
 module BiSpec = BiSpec
-module BranchCase = BranchCase
+module Branch_case = Branch_case
 module Cmd = Cmd
 module Constant = Constant
 module Expr = Expr
diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli
index 4786712fb..0d5190052 100644
--- a/GillianCore/GIL_Syntax/Gil_syntax.mli
+++ b/GillianCore/GIL_Syntax/Gil_syntax.mli
@@ -988,8 +988,8 @@ module BiSpec : sig
   val pp : Format.formatter -> t -> unit
 end
 
-(** @canonical Gillian.Gil_syntax.BranchCase *)
-module BranchCase : sig
+(** @canonical Gillian.Gil_syntax.Branch_case *)
+module Branch_case : sig
   (** Reasons for a branch in execution.
 
     These are used to reason about execution when using the debugger.
@@ -1008,6 +1008,8 @@ module BranchCase : sig
 
     Every termination of a symbolic execution is uniquely identified by its branch path. *)
   type path = t list [@@deriving yojson]
+
+  val pp_short : Format.formatter -> t -> unit
 end
 
 (** @canonical Gillian.Gil_syntax.Annot *)
diff --git a/GillianCore/debugging/debugger/base_debugger.ml b/GillianCore/debugging/debugger/base_debugger.ml
index c7fd8ac60..e43b10d3d 100644
--- a/GillianCore/debugging/debugger/base_debugger.ml
+++ b/GillianCore/debugging/debugger/base_debugger.ml
@@ -2,7 +2,6 @@ open Syntaxes.Option
 module L = Logging
 module DL = Debugger_log
 module Lift = Debugger_lifter
-module Exec_map = Exec_map
 
 let ( let** ) = Result.bind
 let ( let++ ) f o = Result.map o f
@@ -427,6 +426,34 @@ struct
 
     let update_proc_state = Update_proc_state.f
 
+    let jump_state_to_id id cfg state =
+      try
+        DL.log (fun m -> m "Jumping to id %a" L.Report_id.pp id);
+        (* state.exec_map |> snd |> Exec_map.path_of_id id |> ignore; *)
+        (* TODO *)
+        state |> update_proc_state id cfg;
+        Ok ()
+      with Failure msg -> Error msg
+
+    let jump_to_id id (state : t) =
+      let** proc_state = get_proc_state ~cmd_id:id state in
+      jump_state_to_id id state.debug_state proc_state
+
+    let handle_stop debug_state proc_state ?(is_end = false) id id' =
+      let id =
+        match id' with
+        | None -> id
+        | Some id' ->
+            jump_state_to_id id' debug_state proc_state |> Result.get_ok;
+            id
+      in
+      if is_end then
+        let () = DL.log (fun m -> m "STOP (end)") in
+        (ReachedEnd, None)
+      else
+        let () = DL.log (fun m -> m "STOP (%a)" L.Report_id.pp id) in
+        (Step, Some id)
+
     let show_result_errors = function
       | Exec_res.RSucc _ -> []
       | Exec_res.RFail { errors; _ } -> errors |> List.map show_err_t
@@ -447,8 +474,8 @@ struct
 
       type execute_step =
         L.Report_id.t ->
-        ?branch_case:BranchCase.t ->
-        ?branch_path:BranchCase.path ->
+        ?branch_case:Branch_case.t ->
+        ?branch_path:Branch_case.path ->
         debug_state ->
         proc_state ->
         stop_reason * L.Report_id.t option
@@ -469,7 +496,7 @@ struct
         in
         DL.log (fun m ->
             m
-              ~json:[ ("path", BranchCase.path_to_yojson branch_path) ]
+              ~json:[ ("path", Branch_case.path_to_yojson branch_path) ]
               "Got path");
         branch_path
 
@@ -490,10 +517,10 @@ struct
         | ExecNext (id, branch_case) ->
             DL.log (fun m ->
                 m "EXEC NEXT (%a, %a)" (pp_option L.Report_id.pp) id
-                  (pp_option BranchCase.pp) branch_case);
+                  (pp_option Branch_case.pp) branch_case);
             let id = Option_utils.coalesce id default_next_id |> Option.get in
             execute_step id ?branch_case dbg state
-        | Stop -> on_stop ()
+        | Stop id -> on_stop id
 
       module Handle_continue = struct
         let get_report_and_check_type
@@ -540,7 +567,6 @@ struct
                  execute_step ~branch_path cur_report_id debug_state proc_state)
                ~continue:(fun content ->
                  update_proc_state cur_report_id debug_state proc_state;
-                 let open Exec_map in
                  let cmd = content |> of_yojson_string ConfigReport.of_yojson in
                  let cmd_kind = Exec_map.kind_of_cases new_branch_cases in
                  let unifys = get_unifys cur_report_id debug_state proc_state in
@@ -551,10 +577,8 @@ struct
                  proc_state.lifter_state
                  |> Lifter.handle_cmd prev_id_in_frame branch_case exec_data
                  |> handle_lifter_result ~default_next_id:cur_report_id
-                      execute_step debug_state proc_state (fun () ->
-                        DL.log (fun m ->
-                            m "STOP (%a)" L.Report_id.pp cur_report_id);
-                        (Step, Some cur_report_id)))
+                      execute_step debug_state proc_state
+                      (handle_stop debug_state proc_state cur_report_id))
       end
 
       let handle_continue = Handle_continue.f
@@ -594,9 +618,8 @@ struct
           update_proc_state prev_id debug_state proc_state;
           proc_state.lifter_state
           |> Lifter.handle_cmd prev_prev_id cmd.branch_case exec_data
-          |> handle_lifter_result execute_step debug_state proc_state (fun () ->
-                 DL.log (fun m -> m "STOP (end)");
-                 (ReachedEnd, None))
+          |> handle_lifter_result execute_step debug_state proc_state
+               (handle_stop debug_state proc_state ~is_end:true prev_id)
       end
 
       let handle_end_of_branch = Handle_end_of_branch.f
@@ -713,9 +736,8 @@ struct
                let stop_reason, id =
                  handler_result
                  |> Execute_step.handle_lifter_result execute_step
-                      ~default_next_id:id debug_state proc_state (fun () ->
-                        DL.log (fun m -> m "STOP (%a)" L.Report_id.pp id);
-                        (Step, Some id))
+                      ~default_next_id:id debug_state proc_state
+                      (handle_stop debug_state proc_state id)
                in
                let id = id |> Option.get in
                update_proc_state id debug_state proc_state;
@@ -801,19 +823,6 @@ struct
 
     let launch = Launch.f
 
-    let jump_state_to_id id cfg state =
-      try
-        DL.log (fun m -> m "Jumping to id %a" L.Report_id.pp id);
-        (* state.exec_map |> snd |> Exec_map.path_of_id id |> ignore; *)
-        (* TODO *)
-        state |> update_proc_state id cfg;
-        Ok ()
-      with Failure msg -> Error msg
-
-    let jump_to_id id (state : t) =
-      let** proc_state = get_proc_state ~cmd_id:id state in
-      jump_state_to_id id state.debug_state proc_state
-
     let jump_to_start (state : t) =
       let { debug_state; _ } = state in
       let proc_state = get_proc_state_exn state in
@@ -892,7 +901,7 @@ struct
 
       let step_until_cond
           ?(reverse = false)
-          ?(branch_case : BranchCase.t option)
+          ?(branch_case : Branch_case.t option)
           (cond : frame -> frame -> int -> int -> bool)
           (debug_state : debug_state)
           (proc_state : proc_state) : stop_reason =
diff --git a/GillianCore/debugging/debugger/verification_debugger.ml b/GillianCore/debugging/debugger/verification_debugger.ml
index d1e7f06ea..6334a4c77 100644
--- a/GillianCore/debugging/debugger/verification_debugger.ml
+++ b/GillianCore/debugging/debugger/verification_debugger.ml
@@ -55,17 +55,6 @@ struct
 
       let build_unify_map = Build_map.f
 
-      let get_test debug_state proc_name =
-        let tests = debug_state.ext.tests in
-        match tests |> List.assoc_opt proc_name with
-        | None ->
-            DL.failwith
-              (fun () ->
-                let tests_json = Verification.proc_tests_to_yojson tests in
-                [ ("tests", tests_json) ])
-              (Fmt.str "No test found for proc `%s`!" proc_name)
-        | Some test -> test
-
       let is_unify_successful id =
         L.Log_queryer.get_unify_results id
         |> List.exists (fun (_, content) ->
@@ -84,7 +73,7 @@ struct
         (id, content, success)
 
       let f result proc_name prev_id debug_state =
-        let test = get_test debug_state proc_name in
+        let* test = debug_state.ext.tests |> List.assoc_opt proc_name in
         let+ id, content, success =
           match L.Log_queryer.get_unify_for prev_id with
           | Some (id, content) -> Some (id, content, is_unify_successful id)
diff --git a/GillianCore/debugging/lifter/gil_fallback_lifter.ml b/GillianCore/debugging/lifter/gil_fallback_lifter.ml
index f3be8a477..518d4f416 100644
--- a/GillianCore/debugging/lifter/gil_fallback_lifter.ml
+++ b/GillianCore/debugging/lifter/gil_fallback_lifter.ml
@@ -59,13 +59,15 @@ functor
     let dump = to_yojson
 
     let handle_cmd prev_id branch_case exec_data { gil; tl } =
-      (* TODO: defer skipping to TL lifter *)
-      match gil |> Gil_lifter.handle_cmd prev_id branch_case exec_data with
-      | Stop -> (
-          match tl with
-          | None -> Stop
-          | Some tl -> tl |> TLLifter.handle_cmd prev_id branch_case exec_data)
-      | r -> r
+      let () =
+        match gil |> Gil_lifter.handle_cmd prev_id branch_case exec_data with
+        | Stop None -> ()
+        | Stop _ -> failwith "HORROR - Gil_lifter tried to Stop with id!"
+        | _ -> failwith "HORROR - Gil_lifter didn't give Stop!"
+      in
+      match tl with
+      | None -> Stop None
+      | Some tl -> tl |> TLLifter.handle_cmd prev_id branch_case exec_data
 
     let get_gil_map state = state.gil |> Gil_lifter.get_gil_map
 
diff --git a/GillianCore/debugging/lifter/gil_lifter.ml b/GillianCore/debugging/lifter/gil_lifter.ml
index fc32be7e0..62a891064 100644
--- a/GillianCore/debugging/lifter/gil_lifter.ml
+++ b/GillianCore/debugging/lifter/gil_lifter.ml
@@ -5,7 +5,7 @@ open Lifter
 module type S = sig
   include Lifter.S
 
-  val pop_to_exec : t -> (Logging.Report_id.t * BranchCase.t option) option
+  val should_skip_cmd : cmd_report Lifter.executed_cmd_data -> t -> bool
 end
 
 module Make
@@ -22,8 +22,8 @@ module Make
   module Annot = PC.Annot
 
   type annot = PC.Annot.t
-  type branch_case = BranchCase.t [@@deriving yojson]
-  type branch_path = BranchCase.path [@@deriving yojson]
+  type branch_case = Branch_case.t [@@deriving yojson]
+  type branch_path = Branch_case.path [@@deriving yojson]
 
   (* Some fields are Null'd in yojson to stop huge memory inefficiency *)
   type map = (branch_case, cmd_data, unit) Exec_map.t
@@ -44,7 +44,7 @@ module Make
     root_proc : string;
     all_procs : string list;
     id_map : (L.Report_id.t, map) Hashtbl.t; [@to_yojson fun _ -> `Null]
-    mutable to_exec : (L.Report_id.t * BranchCase.t option) list;
+    mutable to_exec : (L.Report_id.t * Branch_case.t option) list;
   }
   [@@deriving to_yojson]
 
@@ -73,22 +73,21 @@ module Make
       () =
     let display = Fmt.to_to_string Cmd.pp_indexed cmd_report.cmd in
     let data = { id; display; unifys; errors; submap; branch_path; parent } in
-    let cmd, to_exec =
+    let cmd =
       match kind with
-      | Normal -> (Cmd { data; next = Nothing }, [ (id, None) ])
+      | Normal -> Cmd { data; next = Nothing }
       | Branch cases ->
           let nexts = Hashtbl.create (List.length cases) in
-          let to_exec =
-            cases
-            |> List.map (fun (case, _) ->
-                   Hashtbl.add nexts case ((), Nothing);
-                   (id, Some case))
+          let () =
+            List.iter
+              (fun (case, _) -> Hashtbl.add nexts case ((), Nothing))
+              cases
           in
-          (BranchCmd { data; nexts }, to_exec)
-      | Final -> (FinalCmd { data }, [])
+          BranchCmd { data; nexts }
+      | Final -> FinalCmd { data }
     in
     Hashtbl.replace id_map id cmd;
-    (cmd, to_exec)
+    cmd
 
   let get_id_opt = function
     | Nothing -> None
@@ -124,27 +123,22 @@ module Make
 
   let init_exn ~proc_name ~all_procs _ _ exec_data =
     let id_map = Hashtbl.create 1 in
-    let map, _ = new_cmd id_map exec_data ~parent:None () in
-    ({ map; root_proc = proc_name; all_procs; id_map; to_exec = [] }, Stop)
+    let map = new_cmd id_map exec_data ~parent:None () in
+    ({ map; root_proc = proc_name; all_procs; id_map; to_exec = [] }, Stop None)
 
   let init ~proc_name ~all_procs tl_ast prog exec_data =
     Some (init_exn ~proc_name ~all_procs tl_ast prog exec_data)
 
   let should_skip_cmd (exec_data : cmd_report executed_cmd_data) state : bool =
-    let annot = exec_data.cmd_report.annot in
-    if Annot.is_hidden annot then (
-      DL.log (fun m -> m "Gil_lifter: skipping hidden cmd");
-      true)
-    else
-      let proc_name = get_proc_name exec_data in
-      if not (List.mem proc_name state.all_procs) then (
-        DL.log (fun m -> m "Gil_lifter: skipping cmd from internal proc");
-        true)
-      else false
+    let proc_name = get_proc_name exec_data in
+    not (List.mem proc_name state.all_procs)
 
   let handle_cmd prev_id branch_case exec_data state =
     let { id_map; _ } = state in
     let new_cmd = new_cmd id_map exec_data in
+    let branch_case =
+      Option_utils.coalesce branch_case exec_data.cmd_report.branch_case
+    in
     let failwith s =
       DL.failwith
         (fun () ->
@@ -162,13 +156,12 @@ module Make
       | None ->
           failwith (Fmt.str "couldn't find prev_id %a!" L.Report_id.pp prev_id)
     in
-    let to_exec =
+    let () =
       match map with
       | Cmd cmd when cmd.next = Nothing ->
           let parent = Some (map, None) in
-          let new_cmd, to_exec = new_cmd ~parent () in
-          cmd.next <- new_cmd;
-          to_exec
+          let new_cmd = new_cmd ~parent () in
+          cmd.next <- new_cmd
       | Cmd _ -> failwith "cmd.next not Nothing!"
       | BranchCmd { nexts; _ } -> (
           match branch_case with
@@ -178,22 +171,15 @@ module Make
               match Hashtbl.find_opt nexts case with
               | Some ((), Nothing) ->
                   let parent = Some (map, Some case) in
-                  let new_cmd, to_exec = new_cmd ~parent () in
-                  Hashtbl.replace nexts case ((), new_cmd);
-                  to_exec
+                  let new_cmd = new_cmd ~parent () in
+                  Hashtbl.replace nexts case ((), new_cmd)
               | Some ((), _) -> failwith "colliding cases in branch cmd"
               | None -> failwith "inserted branch case not found on parent!"))
       | _ -> failwith "can't insert to Nothing or FinalCmd"
     in
-    if should_skip_cmd exec_data state then
-      state.to_exec <- to_exec @ state.to_exec;
-    match state.to_exec with
-    | (id, case) :: rest_to_exec ->
-        state.to_exec <- rest_to_exec;
-        ExecNext (Some id, case)
-    | _ -> Stop
+    Stop None
 
-  let package_case _ case _ = Packaged.package_gil_case case
+  let package_case ~bd:_ ~all_cases:_ case = Packaged.package_gil_case case
 
   let package_data package { id; display; unifys; errors; submap; _ } =
     let submap =
@@ -202,7 +188,7 @@ module Make
       | Proc p -> Proc p
       | Submap map -> Submap (package map)
     in
-    Packaged.{ ids = [ id ]; display; unifys; errors; submap }
+    Packaged.{ id; all_ids = [ id ]; display; unifys; errors; submap }
 
   let package = Packaged.package package_data package_case
   let get_gil_map state = package state.map
@@ -249,11 +235,11 @@ module Make
             in
             List.rev nexts)
 
-  let next_gil_step id case _ =
+  let next_gil_step id (case : Exec_map.Packaged.branch_case option) _ =
     let case =
-      case
-      |> Option.map (fun (case : Exec_map.Packaged.branch_case) ->
-             case.json |> BranchCase.of_yojson |> Result.get_ok)
+      Option.map
+        (fun (_, json) -> json |> Branch_case.of_yojson |> Result.get_ok)
+        case
     in
     (id, case)
 
@@ -351,11 +337,4 @@ module Make
     let () = Hashtbl.replace variables store_id store_vars in
     let () = Hashtbl.replace variables memory_id memory_vars in
     scopes
-
-  let pop_to_exec state =
-    match state.to_exec with
-    | [] -> None
-    | (id, case) :: to_exec ->
-        state.to_exec <- to_exec;
-        Some (id, case)
 end
diff --git a/GillianCore/debugging/lifter/gil_lifter.mli b/GillianCore/debugging/lifter/gil_lifter.mli
index 816117b04..3a3d614de 100644
--- a/GillianCore/debugging/lifter/gil_lifter.mli
+++ b/GillianCore/debugging/lifter/gil_lifter.mli
@@ -3,7 +3,7 @@
 module type S = sig
   include Lifter.S
 
-  val pop_to_exec : t -> (Logging.Report_id.t * BranchCase.t option) option
+  val should_skip_cmd : cmd_report Lifter.executed_cmd_data -> t -> bool
 end
 
 module Make
diff --git a/GillianCore/debugging/lifter/lifter_intf.ml b/GillianCore/debugging/lifter/lifter_intf.ml
index 7d3e4879c..95f2e510a 100644
--- a/GillianCore/debugging/lifter/lifter_intf.ml
+++ b/GillianCore/debugging/lifter/lifter_intf.ml
@@ -10,18 +10,18 @@ module Types = struct
   }
 
   type 'cmd_report executed_cmd_data = {
-    kind : (BranchCase.t, unit) Exec_map.cmd_kind;
+    kind : (Branch_case.t, unit) Exec_map.cmd_kind;
     id : Logging.Report_id.t;
     cmd_report : 'cmd_report;
     unifys : Exec_map.unification list;
     errors : string list;
-    branch_path : BranchCase.path;
+    branch_path : Branch_case.path;
   }
   [@@deriving yojson]
 
   type handle_cmd_result =
-    | Stop
-    | ExecNext of (Logging.Report_id.t option * BranchCase.t option)
+    | Stop of Logging.Report_id.t option
+    | ExecNext of (Logging.Report_id.t option * Branch_case.t option)
   [@@deriving yojson]
 end
 
@@ -66,7 +66,7 @@ module type S = sig
   (** Handles the execution result of a GIL command. *)
   val handle_cmd :
     Logging.Report_id.t ->
-    BranchCase.t option ->
+    Branch_case.t option ->
     cmd_report executed_cmd_data ->
     t ->
     handle_cmd_result
@@ -92,12 +92,14 @@ module type S = sig
   val get_root_id : t -> Logging.Report_id.t option
 
   (** Gives the path of (GIL) branch cases that lead to the specified command. *)
-  val path_of_id : Logging.Report_id.t -> t -> BranchCase.path
+  val path_of_id : Logging.Report_id.t -> t -> Branch_case.path
 
   (** Gets a list of ID/branch-case pairs that correspond to any commands that
     directly succeed the specified command. *)
   val existing_next_steps :
-    Logging.Report_id.t -> t -> (Logging.Report_id.t * BranchCase.t option) list
+    Logging.Report_id.t ->
+    t ->
+    (Logging.Report_id.t * Branch_case.t option) list
 
   (** Translates a command ID and (packaged) TL branch case to the command ID
     and GIL branch case necessary to step forward. *)
@@ -105,7 +107,7 @@ module type S = sig
     Logging.Report_id.t ->
     Exec_map.Packaged.branch_case option ->
     t ->
-    Logging.Report_id.t * BranchCase.t option
+    Logging.Report_id.t * Branch_case.t option
 
   (** If the given command has a previous command, gives its ID, and
     the TL branch case that connects them (if applicable). *)
@@ -118,7 +120,7 @@ module type S = sig
   
     If the given command branches, the desired branch case can be specified. *)
   val select_next_path :
-    BranchCase.t option -> Logging.Report_id.t -> t -> BranchCase.path
+    Branch_case.t option -> Logging.Report_id.t -> t -> Branch_case.path
 
   (** Gives a branch path under the specified command (or the root command, if
     not specified) that hasn't yet been fully explored.
@@ -131,7 +133,7 @@ module type S = sig
   val find_unfinished_path :
     ?at_id:Logging.Report_id.t ->
     t ->
-    (Logging.Report_id.t * BranchCase.t option) option
+    (Logging.Report_id.t * Branch_case.t option) option
 
   val memory_error_to_exception_info :
     (memory_error, annot, tl_ast) memory_error_info -> exception_info
@@ -155,11 +157,11 @@ module type Intf = sig
   module type S = S
 
   val make_executed_cmd_data :
-    (BranchCase.t, unit) Exec_map.cmd_kind ->
+    (Branch_case.t, unit) Exec_map.cmd_kind ->
     Logging.Report_id.t ->
     'cmd_report ->
     ?unifys:Exec_map.unification list ->
     ?errors:string list ->
-    BranchCase.path ->
+    Branch_case.path ->
     'cmd_report executed_cmd_data
 end
diff --git a/GillianCore/debugging/utils/exec_map.ml b/GillianCore/debugging/utils/exec_map.ml
index 2e07589e4..68f34dd32 100644
--- a/GillianCore/debugging/utils/exec_map.ml
+++ b/GillianCore/debugging/utils/exec_map.ml
@@ -135,14 +135,7 @@ let at_path_exn ?(stop_at = EndOfPath) path map =
 
 (** An Exec_map to be passed to the debugger frontend and displayed *)
 module Packaged = struct
-  type branch_case = {
-    kind : string;
-    display : string * string;
-        (** A friendly name for the branch kind and specific branch case to be displayed to the user *)
-    json : Yojson.Safe.t;
-        (** The JSON of the original branch case; this can be target language specific *)
-  }
-  [@@deriving yojson]
+  type branch_case = string * Yojson.Safe.t [@@deriving yojson]
 
   (* Need this to avoid name conflict *)
   (**/**)
@@ -156,7 +149,8 @@ module Packaged = struct
   type t = (branch_case, cmd_data, unit) _map
 
   and cmd_data = {
-    ids : L.Report_id.t list;
+    id : L.Report_id.t;
+    all_ids : L.Report_id.t list;
     display : string;
     unifys : unification list;
     errors : string list;
@@ -165,19 +159,10 @@ module Packaged = struct
   [@@deriving yojson]
 
   (** Converts a GIL branch case to a packaged branch case *)
-  let package_gil_case (case : BranchCase.t) : branch_case =
-    let json = BranchCase.to_yojson case in
-    let kind, display =
-      match case with
-      | GuardedGoto b -> ("GuardedGoto", ("If/Else", Fmt.str "%B" b))
-      | LCmd x -> ("LCmd", ("Logical command", Fmt.str "%d" x))
-      | SpecExec (fl, i) ->
-          ("SpecExec", ("Spec exec", Fmt.str "%a-%d" Flag.pp fl i))
-      | LAction x -> ("LAction", ("Logical action", Fmt.str "L%d" x))
-      | LActionFail x ->
-          ("LActionFail", ("Logical action failure", Fmt.str "LF%d" x))
-    in
-    { kind; display; json }
+  let package_gil_case (case : Branch_case.t) : branch_case =
+    let json = Branch_case.to_yojson case in
+    let display = Fmt.str "%a" Branch_case.pp_short case in
+    (display, json)
 
   (** Converts an Exec_map to a packaged Exec_map *)
   let package package_data package_case (map : ('c, 'd, 'bd) _map) : t =
@@ -195,7 +180,7 @@ module Packaged = struct
           let nexts =
             nexts
             |> Hashtbl.map (fun case (bdata, next) ->
-                   let case = package_case bdata case all_cases in
+                   let case = package_case ~bd:bdata ~all_cases case in
                    let next = aux next in
                    (case, ((), next)))
           in
diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 983a36a12..04c352721 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2021,6 +2021,10 @@ and simplify_int_arithmetic_lexpr
       Cint.to_expr (Cint.plus cl cr)
   | _ -> le
 
+(** Checks if an int expression is greater than zero.
+      
+    @returns [Some true] if definitely > 0, [Some false] if definitely < 0,
+      and [None] if both outcomes are satisfiable. *)
 and check_ge_zero_int ?(top_level = false) (pfs : PFS.t) (e : Expr.t) :
     bool option =
   (* L.verbose (fun fmt -> fmt "Check >= 0: %a" Expr.pp e); *)
@@ -2049,7 +2053,10 @@ and check_ge_zero_int ?(top_level = false) (pfs : PFS.t) (e : Expr.t) :
               | _ -> true
             then result
             else if Expr.equal e' e then None
-            else if Z.gt c Z.zero then f e'
+            else if Z.gt c Z.zero then
+              match f e' with
+              | Some true -> Some true
+              | _ -> None
             else
               match f (UnOp (IUnaryMinus, e')) with
               | Some true -> Some true
@@ -2057,6 +2064,7 @@ and check_ge_zero_int ?(top_level = false) (pfs : PFS.t) (e : Expr.t) :
           ce.symb (Some true)
       else None
 
+(** Same as {!check_ge_zero_int}, but for real number expressions. *)
 and check_ge_zero_num ?(top_level = false) (pfs : PFS.t) (e : Expr.t) :
     bool option =
   (* L.verbose (fun fmt -> fmt "Check >= 0: %a" Expr.pp e); *)
@@ -2080,7 +2088,10 @@ and check_ge_zero_num ?(top_level = false) (pfs : PFS.t) (e : Expr.t) :
           (fun e' c result ->
             if result <> Some true then result
             else if e' = e then None
-            else if c > 0. then f e'
+            else if c > 0. then
+              match f e' with
+              | Some true -> Some true
+              | _ -> None
             else
               match f (UnOp (FUnaryMinus, e')) with
               | Some true -> Some true
diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
index 1afcc2eb7..97bd2400e 100644
--- a/GillianCore/engine/general_semantics/general/g_interpreter.ml
+++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -1,10 +1,10 @@
 open Literal
-open BranchCase
+open Branch_case
 module L = Logging
 module DL = Debugger_log
 include G_interpreter_intf
 
-type branch_case = BranchCase.t [@@deriving yojson]
+type branch_case = Branch_case.t [@@deriving yojson]
 
 (** General GIL Interpreter *)
 module Make
@@ -145,14 +145,14 @@ struct
   type conf_t = BConfErr of err_t list | BConfCont of State.t
   type result_t = (State.t, State.vt, err_t) Exec_res.t [@@deriving yojson]
 
-  type 'result cont_func_f = ?path:BranchCase.path -> unit -> 'result cont_func
+  type 'result cont_func_f = ?path:Branch_case.path -> unit -> 'result cont_func
 
   and 'result cont_func =
     | Finished of 'result list
     | Continue of {
         report_id : Logging.Report_id.t option;
-        branch_path : BranchCase.path;
-        new_branch_cases : BranchCase.t list;
+        branch_path : Branch_case.path;
+        new_branch_cases : Branch_case.t list;
         cont_func : 'result cont_func_f;
       }
     | EndOfBranch of 'result * 'result cont_func_f
diff --git a/GillianCore/engine/general_semantics/general/g_interpreter_intf.ml b/GillianCore/engine/general_semantics/general/g_interpreter_intf.ml
index f76c4c7c7..f83c62bfd 100644
--- a/GillianCore/engine/general_semantics/general/g_interpreter_intf.ml
+++ b/GillianCore/engine/general_semantics/general/g_interpreter_intf.ml
@@ -33,7 +33,7 @@ module type S = sig
       proc_idx : int;
       error_state : state_t;
       errors : err_t list;
-      branch_path : BranchCase.path;
+      branch_path : Branch_case.path;
     }
 
     type cont = {
@@ -45,8 +45,8 @@ module type S = sig
       loop_ids : string list;
       branch_count : int;
       prev_cmd_report_id : Logging.Report_id.t option;
-      branch_case : BranchCase.t option;
-      branch_path : BranchCase.path;
+      branch_case : Branch_case.t option;
+      branch_path : Branch_case.path;
     }
 
     (** Equal to conf_cont + the id of the required spec *)
@@ -54,7 +54,7 @@ module type S = sig
       flag : Flag.t;
       ret_val : state_vt;
       final_state : state_t;
-      branch_path : BranchCase.path;
+      branch_path : Branch_case.path;
     }
 
     type susp = {
@@ -66,7 +66,7 @@ module type S = sig
       next_idx : int;
       loop_ids : string list;
       branch_count : int;
-      branch_path : BranchCase.path;
+      branch_path : Branch_case.path;
     }
 
     type t =
@@ -85,14 +85,14 @@ module type S = sig
 
   (** To support the step-by-step behaviour of the debugger, execution is split into thunks; each invocation executes one GIL command.
     By supplying a branch path, a particular branch of execution can be selected. *)
-  type 'result cont_func_f = ?path:BranchCase.path -> unit -> 'result cont_func
+  type 'result cont_func_f = ?path:Branch_case.path -> unit -> 'result cont_func
 
   and 'result cont_func =
     | Finished of 'result list
     | Continue of {
         report_id : Logging.Report_id.t option;
-        branch_path : BranchCase.path;
-        new_branch_cases : BranchCase.t list;
+        branch_path : Branch_case.path;
+        new_branch_cases : Branch_case.t list;
         cont_func : 'result cont_func_f;
       }
     | EndOfBranch of 'result * 'result cont_func_f
@@ -108,7 +108,7 @@ module type S = sig
         annot : annot;
         branching : int;
         state : state_t;
-        branch_case : BranchCase.t option;
+        branch_case : Branch_case.t option;
         proc_name : string;
       }
       [@@deriving yojson]
@@ -123,7 +123,7 @@ module type S = sig
         proc_body_index : int;
         state : state_t option;
         errors : err_t list;
-        branch_case : BranchCase.t option;
+        branch_case : Branch_case.t option;
       }
       [@@deriving yojson]
     end
diff --git a/GillianCore/utils/ext_list.ml b/GillianCore/utils/ext_list.ml
index 58b20ab3a..bac4eddec 100644
--- a/GillianCore/utils/ext_list.ml
+++ b/GillianCore/utils/ext_list.ml
@@ -33,6 +33,7 @@ let append x l =
       l.last <- cell
 
 let add = append
+let add_all xs t = List.iter (fun x -> add x t) xs
 let length t = t.length
 
 let to_list t =
@@ -210,6 +211,14 @@ let exists f l =
   in
   aux l.first
 
+let assoc_opt a l =
+  let rec aux = function
+    | Nil -> None
+    | Cons { contents = k, v; _ } when a = k -> Some v
+    | Cons { next; _ } -> aux next
+  in
+  aux l.first
+
 let nth n l =
   if n >= l.length || n < 0 then None
   else
diff --git a/GillianCore/utils/ext_list.mli b/GillianCore/utils/ext_list.mli
index 28992b4cb..641ef5ebc 100644
--- a/GillianCore/utils/ext_list.mli
+++ b/GillianCore/utils/ext_list.mli
@@ -11,6 +11,7 @@ val clear : 'a t -> unit
 val prepend : 'a -> 'a t -> unit
 val append : 'a -> 'a t -> unit
 val add : 'a -> 'a t -> unit
+val add_all : 'a list -> 'a t -> unit
 val length : 'a t -> int
 val to_list : 'a t -> 'a list
 val of_list : 'a list -> 'a t
@@ -31,6 +32,7 @@ val iter : ('a -> unit) -> 'a t -> unit
 val for_all2 : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
 
 val exists : ('a -> bool) -> 'a t -> bool
+val assoc_opt : 'a -> ('a * 'b) t -> 'b option
 val remove_duplicates : ?equal:('a -> 'a -> bool) -> 'a t -> unit
 
 (** Filter-maps the list in place according to [f]
diff --git a/GillianCore/utils/list_utils.ml b/GillianCore/utils/list_utils.ml
index f2f129002..fff1fbafa 100644
--- a/GillianCore/utils/list_utils.ml
+++ b/GillianCore/utils/list_utils.ml
@@ -175,6 +175,16 @@ let map_results f l =
   in
   aux [] l
 
+let iter_results f l =
+  let rec aux = function
+    | [] -> Ok ()
+    | x :: xs -> (
+        match f x with
+        | Ok () -> aux xs
+        | Error e -> Error e)
+  in
+  aux l
+
 let for_alli f l =
   let rec aux i = function
     | [] -> true
diff --git a/GillianCore/utils/result_utils.ml b/GillianCore/utils/result_utils.ml
index a9461bec3..f5e1f0a73 100644
--- a/GillianCore/utils/result_utils.ml
+++ b/GillianCore/utils/result_utils.ml
@@ -2,3 +2,7 @@ let of_option ~none x =
   match x with
   | None -> Error none
   | Some x -> Ok x
+
+let or_else f = function
+  | Ok x -> x
+  | Error e -> f e
diff --git a/GillianCore/utils/result_utils.mli b/GillianCore/utils/result_utils.mli
deleted file mode 100644
index ffb83a855..000000000
--- a/GillianCore/utils/result_utils.mli
+++ /dev/null
@@ -1 +0,0 @@
-val of_option : none:'b -> 'a option -> ('a, 'b) Result.t
diff --git a/GillianCore/utils/syntaxes.ml b/GillianCore/utils/syntaxes.ml
index 5f207721c..de8a5d79f 100644
--- a/GillianCore/utils/syntaxes.ml
+++ b/GillianCore/utils/syntaxes.ml
@@ -16,8 +16,43 @@ end
 
 (** @canonical Gillian.Utils.Syntaxes.Option *)
 module Option = struct
-  let ( let+ ) f o = Option.map o f
+  let ( let+ ) o f = Option.map f o
   let ( let* ) o f = Option.bind o f
+
+  let ( let- ) o f =
+    match o with
+    | None -> f ()
+    | Some o -> o
+
+  let ( let/ ) o f =
+    match o with
+    | None -> f ()
+    | o -> o
+end
+
+(** @canonical Gillian.Utils.Syntaxes.Result_of_option *)
+module Result_of_option = struct
+  let ( let=* ) o f =
+    match o with
+    | Ok (Some o) -> f o
+    | Ok None -> Ok None
+    | Error e -> Error e
+
+  let ( let=+ ) o f =
+    match o with
+    | Ok (Some o) -> Ok (Some (f o))
+    | Ok None -> Ok None
+    | Error e -> Error e
+
+  let ( let=/ ) o f =
+    match o with
+    | Ok None -> f ()
+    | o -> o
+
+  let ( let=- ) o f =
+    match o with
+    | Ok None -> Ok (Some (f ()))
+    | o -> o
 end
 
 (** @canonical Gillian.Utils.Syntaxes.List *)
diff --git a/GillianCore/z3/z3_encoding.ml b/GillianCore/z3/z3_encoding.ml
index 2cdd4fe46..296f287a7 100644
--- a/GillianCore/z3/z3_encoding.ml
+++ b/GillianCore/z3/z3_encoding.ml
@@ -856,7 +856,9 @@ let dump_smt =
     let created = ref false in
     let create () =
       created := true;
-      Unix.mkdir folder_name 0o755
+      try Unix.mkdir folder_name 0o755 with
+      | Unix.Unix_error (Unix.EEXIST, _, _) -> ()
+      | e -> raise e
     in
     fun () ->
       let () = if not !created then create () in
diff --git a/debugger-vscode-extension/package.json b/debugger-vscode-extension/package.json
index a9eb7d126..c7f20e3b9 100644
--- a/debugger-vscode-extension/package.json
+++ b/debugger-vscode-extension/package.json
@@ -152,6 +152,16 @@
           "type": "boolean",
           "default": false,
           "description": "Enables manual proof mode, i.e. disables automatical folding/unfolding."
+        },
+        "gillianDebugger.showVerifyLens": {
+          "type": "boolean",
+          "default": true,
+          "description": "Shows 'Verify' buttons by verifyable functions."
+        },
+        "gillianDebugger.showSymbolicDebugLens": {
+          "type": "boolean",
+          "default": true,
+          "description": "Shows 'Symbolic-debug' buttons by symbolically-debuggable functions."
         }
       }
     },
diff --git a/debugger-vscode-extension/sampleWorkspace/wisl_demo/sll/manual.wisl b/debugger-vscode-extension/sampleWorkspace/wisl_demo/sll/manual.wisl
index f6d9cfe62..65da031b8 100644
--- a/debugger-vscode-extension/sampleWorkspace/wisl_demo/sll/manual.wisl
+++ b/debugger-vscode-extension/sampleWorkspace/wisl_demo/sll/manual.wisl
@@ -318,9 +318,9 @@ function SLL_append_node_iter(x, y){
            (#vx == #vs1 @ (#v :: #vs2)) ]];
     while(not (next = null)){
       prev := next;
-      next := [next + 1];
+      next := [next + 1]
     };
-    [prev + 1] := y;
+    [prev + 1] := y
   };
   return x
 }
@@ -342,7 +342,7 @@ function SLL_concat_iter(x, y){
         prev := next;
         next := [next + 1]
     };
-    [prev + 1] := y;
+    [prev + 1] := y
   };
   return head
 }
@@ -370,8 +370,8 @@ function SLL_copy_iter(x){
             [c] := v;
             [p + 1] := c;
             p := c;
-            t := [t + 1];
-        };
+            t := [t + 1]
+        }
     };
     return y
 }
diff --git a/debugger-vscode-extension/src/WebviewPanel.ts b/debugger-vscode-extension/src/WebviewPanel.ts
index ea55a44ff..06ee55ded 100644
--- a/debugger-vscode-extension/src/WebviewPanel.ts
+++ b/debugger-vscode-extension/src/WebviewPanel.ts
@@ -77,6 +77,11 @@ export class WebviewPanel {
     }
   }
 
+  public clearState() {
+    console.info('Clearing webview state')
+    this.sendMessage({ type: 'clear_state' })
+  }
+
   public updateState(state: DebuggerState) {
     console.info('Got state', state);
     this.sendMessage({ type: 'state_update', state });
diff --git a/debugger-vscode-extension/src/activateCodeLens.ts b/debugger-vscode-extension/src/activateCodeLens.ts
index 7d6b58290..f89b229d2 100644
--- a/debugger-vscode-extension/src/activateCodeLens.ts
+++ b/debugger-vscode-extension/src/activateCodeLens.ts
@@ -6,6 +6,7 @@ import {
   languages,
   Range,
   TextDocument,
+  workspace,
 } from 'vscode';
 import { startDebugging } from './commands';
 import { ExecMode } from './types';
@@ -52,10 +53,12 @@ class DebugCodeLensProvider implements CodeLensProvider {
 
     const reProcedureName = /(.+?)\(/g;
 
-    const lensKinds: [ExecMode, string][] = [
-      ['debugverify', 'Verify '],
-      ['debugwpst', 'Symbolic-debug '],
-    ];
+    const config = workspace.getConfiguration('gillianDebugger');
+    const lensKinds: [ExecMode, string][] = [];
+    if (config.showVerifyLens)
+      lensKinds.push(['debugverify', 'Verify ']);
+    if (config.showSymbolicDebugLens)
+      lensKinds.push(['debugwpst', 'Symbolic-debug ']);
     const lenses: CodeLens[] = [];
     while (reProcedure.exec(text) !== null) {
       reProcedureName.lastIndex = reProcedure.lastIndex;
diff --git a/debugger-vscode-extension/src/extension.ts b/debugger-vscode-extension/src/extension.ts
index d1c4dc745..c19b9e4c1 100644
--- a/debugger-vscode-extension/src/extension.ts
+++ b/debugger-vscode-extension/src/extension.ts
@@ -9,6 +9,7 @@ import { ProviderResult } from 'vscode';
 import { activateCodeLens } from './activateCodeLens';
 import { activateDebug } from './debug';
 import vscodeVariables from './vscodeVariables';
+import { WebviewPanel } from './WebviewPanel';
 
 export function activate(context: vscode.ExtensionContext) {
   activateDebug(context, new DebugAdapterExecutableFactory());
@@ -101,6 +102,7 @@ class DebugAdapterExecutableFactory
     }
 
     console.log('Starting debugger...', { cmd, args, cwd });
+    WebviewPanel.currentPanel?.clearState();
     const options = { cwd };
     executable = new vscode.DebugAdapterExecutable(cmd, args, options);
 
diff --git a/debugger-vscode-extension/src/types.d.ts b/debugger-vscode-extension/src/types.d.ts
index 5146098d1..1e819a672 100644
--- a/debugger-vscode-extension/src/types.d.ts
+++ b/debugger-vscode-extension/src/types.d.ts
@@ -1,10 +1,6 @@
 // #region ExecMap
 
-export type BranchCase = {
-  readonly kind: string;
-  readonly display: [string, string];
-  readonly json: any;
-};
+export type BranchCase = [string, any];
 
 type Submap =
   | readonly ['NoSubmap']
@@ -18,7 +14,8 @@ type Unification = {
 };
 
 export type CmdData = {
-  readonly ids: readonly number[];
+  readonly id: readonly number;
+  readonly all_ids: readonly number[];
   readonly display: string;
   readonly unifys: readonly Unification[];
   readonly errors: readonly string[];
@@ -121,7 +118,11 @@ type ResetViewMsg = {
   readonly type: 'reset_view';
 };
 
-export type MessageToWebview = StateUpdateMsg | UnifyUpdateMsg | ResetViewMsg;
+type ClearStateMsg = {
+  readonly type: 'clear_state';
+}
+
+export type MessageToWebview = StateUpdateMsg | UnifyUpdateMsg | ResetViewMsg | ClearStateMsg;
 
 // #endregion
 
diff --git a/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapView.tsx b/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapView.tsx
index 83cc4f864..ea1965aad 100644
--- a/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapView.tsx
+++ b/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapView.tsx
@@ -53,8 +53,8 @@ const ExecMapView = ({ state, expandedNodes, toggleNodeExpanded }: Props) => {
     const { procName, branchCase = null, hasParent = true } = aux;
     const procState = procs[procName];
     const edgeLabel =
-      branchCase && branchCase.display[1] ? (
-        <>{branchCase.display[1]}</>
+      branchCase && branchCase[0] ? (
+        <>{branchCase[0]}</>
       ) : undefined;
     const isActive = procName === currentProcName;
 
@@ -90,7 +90,7 @@ const ExecMapView = ({ state, expandedNodes, toggleNodeExpanded }: Props) => {
       }
     })();
 
-    const id = `${cmdData.ids[0]}`;
+    const id = `${cmdData.id}`;
     const expanded = expandedNodes.has(id);
 
     let hasSubmap = false;
@@ -143,7 +143,7 @@ const ExecMapView = ({ state, expandedNodes, toggleNodeExpanded }: Props) => {
 
     const isCurrentCmd =
       procName === currentProcName &&
-      cmdData.ids.includes(procState.currentCmdId);
+      cmdData.all_ids.includes(procState.currentCmdId);
 
     return {
       id,
@@ -155,7 +155,7 @@ const ExecMapView = ({ state, expandedNodes, toggleNodeExpanded }: Props) => {
         hasParent,
         isActive,
         jump: () => {
-          jumpToId(cmdData.ids[0]);
+          jumpToId(cmdData.id);
         },
         expanded,
         toggleExpanded,
diff --git a/debugger-vscode-extension/src/webviews/src/index.tsx b/debugger-vscode-extension/src/webviews/src/index.tsx
index ee3a548df..02cd56207 100644
--- a/debugger-vscode-extension/src/webviews/src/index.tsx
+++ b/debugger-vscode-extension/src/webviews/src/index.tsx
@@ -24,12 +24,12 @@ VSCodeAPI.onMessage(e => {
     } else {
       store.clearUnification();
     }
-  }
-
-  if (message.type === 'unify_update') {
+  } else if (message.type === 'unify_update') {
     store.loadUnification(message.unifyId, message.unifyMap);
   } else if (message.type === 'reset_view') {
     events.publish('resetView');
+  } else if (message.type === 'clear_state') {
+    store.clear();
   }
 });
 
diff --git a/debugger-vscode-extension/src/webviews/src/store.tsx b/debugger-vscode-extension/src/webviews/src/store.tsx
index 6c45e0ae2..1c15b6606 100644
--- a/debugger-vscode-extension/src/webviews/src/store.tsx
+++ b/debugger-vscode-extension/src/webviews/src/store.tsx
@@ -22,6 +22,7 @@ export type Store = State & {
   selectUnifyStep: (step: UnifyStep) => void;
   toggleExecNodeExpanded: (id: string) => void;
   toggleUnifyNodeExpanded: (id: number) => void;
+  clear: () => void;
 };
 
 const useStore = create<Store>(
@@ -97,6 +98,15 @@ const useStore = create<Store>(
           else expandedNodes.add(id);
         });
       },
+      clear: () => {
+        set((state) => {
+          state.debuggerState = undefined;
+          state.unifyState.path = [];
+          state.unifyState.unifications = {};
+          state.unifyState.expandedNodes.clear();
+          state.expandedExecNodes.clear();
+        })
+      },
     };
   })
 );
diff --git a/esy.json b/esy.json
index 2d2be1352..f7ee11e8b 100644
--- a/esy.json
+++ b/esy.json
@@ -94,7 +94,7 @@
     "@opam/visitors": ">=2.3",
     "@opam/yojson": "^1.7.0",
     "@opam/zarith": ">=1.12",
-    "@opam/z3": "GillianPlatform/esy-z3#37b3fae3f019bd331a5f3cf22ffa193af1a0cdc2",
+    "@opam/z3": "GillianPlatform/esy-z3#e8b2ce266d5d8bd67c54bd226c6301f7b180bb09",
     "compcert": "giltho/CompCert#3a6f14016f0c9aaab2ddcdd61492e5fe54f12259",
     "ocaml": "4.14.x"
   },
diff --git a/esy.lock/index.json b/esy.lock/index.json
index 2659de0cc..90bb882f5 100644
--- a/esy.lock/index.json
+++ b/esy.lock/index.json
@@ -1,5 +1,5 @@
 {
-  "checksum": "122100d5b64171817b3864785e4e7fdb",
+  "checksum": "0ea4b73f304f439e4b1cfbd5d4a37e34",
   "root": "gillian-platform@link-dev:./esy.json",
   "node": {
     "yargs-parser@21.1.1@d41d8cd9": {
@@ -290,8 +290,8 @@
         "ocaml@4.14.1000@d41d8cd9",
         "compcert@github:giltho/CompCert#3a6f14016f0c9aaab2ddcdd61492e5fe54f12259@d41d8cd9",
         "@opam/zarith@opam:1.13@e4e498f3",
-        "@opam/z3@archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.2.tar.gz#md5:4061317f7948c19abd13041c5a32b057@ee5be9c1",
-        "@opam/yojson@opam:2.1.1@ad5e299c",
+        "@opam/z3@archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.3.tar.gz#md5:a18ea8cc1ba59d87a6ea966227732038@44ff3c39",
+        "@opam/yojson@opam:2.1.2@9fd14300",
         "@opam/visitors@opam:20210608@7b4a1100",
         "@opam/uuidm@opam:0.9.7@a349b245",
         "@opam/sqlite3@opam:5.0.2@f8405319",
@@ -311,7 +311,7 @@
         "ocaml@4.14.1000@d41d8cd9", "concurrently@7.6.0@d41d8cd9",
         "@opam/utop@opam:2.13.1@dc6689f5",
         "@opam/shexp@opam:v0.14.0@f803f1bd",
-        "@opam/odoc@opam:2.2.1@1a25cd5a",
+        "@opam/odoc@opam:2.2.2@a43a5ec4",
         "@opam/ocamlformat@opam:0.24.1@d7f4254d",
         "@opam/ocamlfind@opam:1.9.6@da5169c7",
         "@opam/ocaml-lsp-server@opam:1.12.2@7e7be5b8",
@@ -390,7 +390,7 @@
         ]
       },
       "overrides": [],
-      "dependencies": [ "@babel/runtime@7.23.2@d41d8cd9" ],
+      "dependencies": [ "@babel/runtime@7.23.5@d41d8cd9" ],
       "devDependencies": []
     },
     "concurrently@7.6.0@d41d8cd9": {
@@ -584,19 +584,19 @@
         "@opam/conf-gmp@opam:4@862d40a8"
       ]
     },
-    "@opam/z3@archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.2.tar.gz#md5:4061317f7948c19abd13041c5a32b057@ee5be9c1": {
+    "@opam/z3@archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.3.tar.gz#md5:a18ea8cc1ba59d87a6ea966227732038@44ff3c39": {
       "id":
-        "@opam/z3@archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.2.tar.gz#md5:4061317f7948c19abd13041c5a32b057@ee5be9c1",
+        "@opam/z3@archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.3.tar.gz#md5:a18ea8cc1ba59d87a6ea966227732038@44ff3c39",
       "name": "@opam/z3",
       "version":
-        "archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.2.tar.gz#md5:4061317f7948c19abd13041c5a32b057",
+        "archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.3.tar.gz#md5:a18ea8cc1ba59d87a6ea966227732038",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.2.tar.gz#md5:4061317f7948c19abd13041c5a32b057"
+          "archive:https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.3.tar.gz#md5:a18ea8cc1ba59d87a6ea966227732038"
         ]
       },
-      "overrides": [ "esy.lock/overrides/ee5be9c1213cfc9c8d43f4061c829e80" ],
+      "overrides": [ "esy.lock/overrides/44ff3c39826df68739c4470881a91b5f" ],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/zarith@opam:1.13@e4e498f3",
         "@opam/ocamlfind@opam:1.9.6@da5169c7",
@@ -605,20 +605,20 @@
       ],
       "devDependencies": []
     },
-    "@opam/yojson@opam:2.1.1@ad5e299c": {
-      "id": "@opam/yojson@opam:2.1.1@ad5e299c",
+    "@opam/yojson@opam:2.1.2@9fd14300": {
+      "id": "@opam/yojson@opam:2.1.2@9fd14300",
       "name": "@opam/yojson",
-      "version": "opam:2.1.1",
+      "version": "opam:2.1.2",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/d5/d58183207b198dc065866239066e074c34f9e139c0d9c4175a38809790e88173#sha256:d58183207b198dc065866239066e074c34f9e139c0d9c4175a38809790e88173",
-          "archive:https://github.com/ocaml-community/yojson/releases/download/2.1.1/yojson-2.1.1.tbz#sha256:d58183207b198dc065866239066e074c34f9e139c0d9c4175a38809790e88173"
+          "archive:https://opam.ocaml.org/cache/sha256/59/59f2f1abbfc8a7ccbdbf608894e5c75e8a76006e34899254446f83e200dfb4f9#sha256:59f2f1abbfc8a7ccbdbf608894e5c75e8a76006e34899254446f83e200dfb4f9",
+          "archive:https://github.com/ocaml-community/yojson/releases/download/2.1.2/yojson-2.1.2.tbz#sha256:59f2f1abbfc8a7ccbdbf608894e5c75e8a76006e34899254446f83e200dfb4f9"
         ],
         "opam": {
           "name": "yojson",
-          "version": "2.1.1",
-          "path": "esy.lock/opam/yojson.2.1.1"
+          "version": "2.1.2",
+          "path": "esy.lock/opam/yojson.2.1.2"
         }
       },
       "overrides": [],
@@ -632,20 +632,20 @@
         "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
-    "@opam/xdg@opam:3.11.1@1e207b0b": {
-      "id": "@opam/xdg@opam:3.11.1@1e207b0b",
+    "@opam/xdg@opam:3.12.1@36e9c532": {
+      "id": "@opam/xdg@opam:3.12.1@36e9c532",
       "name": "@opam/xdg",
-      "version": "opam:3.11.1",
+      "version": "opam:3.12.1",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/86/866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71",
-          "archive:https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
+          "archive:https://opam.ocaml.org/cache/sha256/b9/b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f",
+          "archive:https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
         ],
         "opam": {
           "name": "xdg",
-          "version": "3.11.1",
-          "path": "esy.lock/opam/xdg.3.11.1"
+          "version": "3.12.1",
+          "path": "esy.lock/opam/xdg.3.12.1"
         }
       },
       "overrides": [],
@@ -838,7 +838,7 @@
       "overrides": [],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/zed@opam:3.2.3@57ab913c",
-        "@opam/xdg@opam:3.11.1@1e207b0b", "@opam/react@opam:1.2.2@e0f4480e",
+        "@opam/xdg@opam:3.12.1@36e9c532", "@opam/react@opam:1.2.2@e0f4480e",
         "@opam/ocamlfind@opam:1.9.6@da5169c7",
         "@opam/lwt_react@opam:1.2.0@4253a145",
         "@opam/lwt@opam:5.7.0@4a33823d", "@opam/logs@opam:0.7.0@46a3dffc",
@@ -850,7 +850,7 @@
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/zed@opam:3.2.3@57ab913c",
-        "@opam/xdg@opam:3.11.1@1e207b0b", "@opam/react@opam:1.2.2@e0f4480e",
+        "@opam/xdg@opam:3.12.1@36e9c532", "@opam/react@opam:1.2.2@e0f4480e",
         "@opam/ocamlfind@opam:1.9.6@da5169c7",
         "@opam/lwt_react@opam:1.2.0@4253a145",
         "@opam/lwt@opam:5.7.0@4a33823d", "@opam/logs@opam:0.7.0@46a3dffc",
@@ -1009,35 +1009,35 @@
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/base@opam:v0.14.3@b3ddb868"
       ]
     },
-    "@opam/stdune@opam:3.11.1@9a840882": {
-      "id": "@opam/stdune@opam:3.11.1@9a840882",
+    "@opam/stdune@opam:3.12.1@2a177cb9": {
+      "id": "@opam/stdune@opam:3.12.1@2a177cb9",
       "name": "@opam/stdune",
-      "version": "opam:3.11.1",
+      "version": "opam:3.12.1",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/86/866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71",
-          "archive:https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
+          "archive:https://opam.ocaml.org/cache/sha256/b9/b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f",
+          "archive:https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
         ],
         "opam": {
           "name": "stdune",
-          "version": "3.11.1",
-          "path": "esy.lock/opam/stdune.3.11.1"
+          "version": "3.12.1",
+          "path": "esy.lock/opam/stdune.3.12.1"
         }
       },
       "overrides": [],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/pp@opam:1.2.0@16430027",
-        "@opam/ordering@opam:3.11.1@92c57daa",
-        "@opam/dyn@opam:3.11.1@d3c74846", "@opam/dune@opam:3.8.3@ff88b4c5",
+        "@opam/ordering@opam:3.12.1@9f3171ff",
+        "@opam/dyn@opam:3.12.1@7b80464e", "@opam/dune@opam:3.8.3@ff88b4c5",
         "@opam/csexp@opam:1.5.2@46614bf4",
         "@opam/base-unix@opam:base@87d0b2eb",
         "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/pp@opam:1.2.0@16430027",
-        "@opam/ordering@opam:3.11.1@92c57daa",
-        "@opam/dyn@opam:3.11.1@d3c74846", "@opam/dune@opam:3.8.3@ff88b4c5",
+        "@opam/ordering@opam:3.12.1@9f3171ff",
+        "@opam/dyn@opam:3.12.1@7b80464e", "@opam/dune@opam:3.8.3@ff88b4c5",
         "@opam/csexp@opam:1.5.2@46614bf4",
         "@opam/base-unix@opam:base@87d0b2eb"
       ]
@@ -1113,14 +1113,14 @@
       "overrides": [],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5",
         "@opam/conf-sqlite3@archive:https://sqlite.org/2021/sqlite-autoconf-3350500.tar.gz#sha256:f52b72a5c319c3e516ed7a92e123139a6e87af08a2dc43d7757724f6132e6db0@2d70a362",
         "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
@@ -1245,12 +1245,12 @@
       "overrides": [],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/uchar@opam:0.0.2@aedf91f9",
-        "@opam/ppxlib@opam:0.25.1@bd0b93cc", "@opam/gen@opam:1.1@059b2731",
+        "@opam/ppxlib@opam:0.25.1@bd0b93cc", "@opam/gen@opam:1.1@55327887",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/uchar@opam:0.0.2@aedf91f9",
-        "@opam/ppxlib@opam:0.25.1@bd0b93cc", "@opam/gen@opam:1.1@059b2731",
+        "@opam/ppxlib@opam:0.25.1@bd0b93cc", "@opam/gen@opam:1.1@55327887",
         "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
@@ -1409,11 +1409,11 @@
       },
       "overrides": [],
       "dependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.1@ad5e299c",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.2@9fd14300",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.1@ad5e299c",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.2@9fd14300",
         "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
@@ -1695,14 +1695,14 @@
       },
       "overrides": [],
       "dependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.1@ad5e299c",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.2@9fd14300",
         "@opam/result@opam:1.5@1c6a6533",
         "@opam/ppxlib@opam:0.25.1@bd0b93cc",
         "@opam/ppx_deriving@opam:5.2.1@2315fdd0",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.1@ad5e299c",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.2@9fd14300",
         "@opam/result@opam:1.5@1c6a6533",
         "@opam/ppxlib@opam:0.25.1@bd0b93cc",
         "@opam/ppx_deriving@opam:5.2.1@2315fdd0",
@@ -1950,20 +1950,20 @@
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/base@opam:v0.14.3@b3ddb868"
       ]
     },
-    "@opam/ordering@opam:3.11.1@92c57daa": {
-      "id": "@opam/ordering@opam:3.11.1@92c57daa",
+    "@opam/ordering@opam:3.12.1@9f3171ff": {
+      "id": "@opam/ordering@opam:3.12.1@9f3171ff",
       "name": "@opam/ordering",
-      "version": "opam:3.11.1",
+      "version": "opam:3.12.1",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/86/866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71",
-          "archive:https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
+          "archive:https://opam.ocaml.org/cache/sha256/b9/b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f",
+          "archive:https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
         ],
         "opam": {
           "name": "ordering",
-          "version": "3.11.1",
-          "path": "esy.lock/opam/ordering.3.11.1"
+          "version": "3.12.1",
+          "path": "esy.lock/opam/ordering.3.12.1"
         }
       },
       "overrides": [],
@@ -2035,20 +2035,20 @@
         "@opam/astring@opam:0.8.5@1300cee8"
       ]
     },
-    "@opam/odoc@opam:2.2.1@1a25cd5a": {
-      "id": "@opam/odoc@opam:2.2.1@1a25cd5a",
+    "@opam/odoc@opam:2.2.2@a43a5ec4": {
+      "id": "@opam/odoc@opam:2.2.2@a43a5ec4",
       "name": "@opam/odoc",
-      "version": "opam:2.2.1",
+      "version": "opam:2.2.2",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/17/1786e53bf0824fe1c7c7b81d2a7d846846a5d11677969e6396361f77a3816803#sha256:1786e53bf0824fe1c7c7b81d2a7d846846a5d11677969e6396361f77a3816803",
-          "archive:https://github.com/ocaml/odoc/releases/download/2.2.1/odoc-2.2.1.tbz#sha256:1786e53bf0824fe1c7c7b81d2a7d846846a5d11677969e6396361f77a3816803"
+          "archive:https://opam.ocaml.org/cache/sha256/6e/6ec331a1da22ec8b8feca73d4b8b6269043f4b36b10dd49f557f42449633672b#sha256:6ec331a1da22ec8b8feca73d4b8b6269043f4b36b10dd49f557f42449633672b",
+          "archive:https://github.com/ocaml/odoc/releases/download/2.2.2/odoc-2.2.2.tbz#sha256:6ec331a1da22ec8b8feca73d4b8b6269043f4b36b10dd49f557f42449633672b"
         ],
         "opam": {
           "name": "odoc",
-          "version": "2.2.1",
-          "path": "esy.lock/opam/odoc.2.2.1"
+          "version": "2.2.2",
+          "path": "esy.lock/opam/odoc.2.2.2"
         }
       },
       "overrides": [],
@@ -2212,7 +2212,7 @@
         "@opam/fpath@opam:0.7.3@674d8125",
         "@opam/fix@opam:20230505@941a65ff",
         "@opam/either@opam:1.0.0@be5a1416",
-        "@opam/dune-build-info@opam:3.11.1@0dfbdab2",
+        "@opam/dune-build-info@opam:3.12.1@ce69ef3d",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/csexp@opam:1.5.2@46614bf4",
         "@opam/cmdliner@opam:1.2.0@b0c6143c",
         "@opam/base@opam:v0.14.3@b3ddb868",
@@ -2231,7 +2231,7 @@
         "@opam/fpath@opam:0.7.3@674d8125",
         "@opam/fix@opam:20230505@941a65ff",
         "@opam/either@opam:1.0.0@be5a1416",
-        "@opam/dune-build-info@opam:3.11.1@0dfbdab2",
+        "@opam/dune-build-info@opam:3.12.1@ce69ef3d",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/csexp@opam:1.5.2@46614bf4",
         "@opam/cmdliner@opam:1.2.0@b0c6143c",
         "@opam/base@opam:v0.14.3@b3ddb868"
@@ -2368,36 +2368,36 @@
       },
       "overrides": [],
       "dependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.1@ad5e299c",
-        "@opam/xdg@opam:3.11.1@1e207b0b", "@opam/uutf@opam:1.0.3@47c95a18",
-        "@opam/stdune@opam:3.11.1@9a840882",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.2@9fd14300",
+        "@opam/xdg@opam:3.12.1@36e9c532", "@opam/uutf@opam:1.0.3@47c95a18",
+        "@opam/stdune@opam:3.12.1@2a177cb9",
         "@opam/spawn@opam:v0.15.1@85e9d6f1", "@opam/re@opam:1.11.0@87deb463",
         "@opam/ppx_yojson_conv_lib@opam:v0.16.0@33740c3c",
         "@opam/pp@opam:1.2.0@16430027",
-        "@opam/ordering@opam:3.11.1@92c57daa",
+        "@opam/ordering@opam:3.12.1@9f3171ff",
         "@opam/omd@opam:1.3.1@1e66b1fa",
         "@opam/octavius@opam:1.2.2@2205cc65",
         "@opam/ocamlformat-rpc-lib@opam:0.26.1@1f552fda",
-        "@opam/fiber@opam:3.7.0@d70e2471", "@opam/dyn@opam:3.11.1@d3c74846",
-        "@opam/dune-rpc@opam:3.11.1@1197fefa",
-        "@opam/dune-build-info@opam:3.11.1@0dfbdab2",
+        "@opam/fiber@opam:3.7.0@d70e2471", "@opam/dyn@opam:3.12.1@7b80464e",
+        "@opam/dune-rpc@opam:3.12.1@03e71e5d",
+        "@opam/dune-build-info@opam:3.12.1@ce69ef3d",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/csexp@opam:1.5.2@46614bf4",
         "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.1@ad5e299c",
-        "@opam/xdg@opam:3.11.1@1e207b0b", "@opam/uutf@opam:1.0.3@47c95a18",
-        "@opam/stdune@opam:3.11.1@9a840882",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.2@9fd14300",
+        "@opam/xdg@opam:3.12.1@36e9c532", "@opam/uutf@opam:1.0.3@47c95a18",
+        "@opam/stdune@opam:3.12.1@2a177cb9",
         "@opam/spawn@opam:v0.15.1@85e9d6f1", "@opam/re@opam:1.11.0@87deb463",
         "@opam/ppx_yojson_conv_lib@opam:v0.16.0@33740c3c",
         "@opam/pp@opam:1.2.0@16430027",
-        "@opam/ordering@opam:3.11.1@92c57daa",
+        "@opam/ordering@opam:3.12.1@9f3171ff",
         "@opam/omd@opam:1.3.1@1e66b1fa",
         "@opam/octavius@opam:1.2.2@2205cc65",
         "@opam/ocamlformat-rpc-lib@opam:0.26.1@1f552fda",
-        "@opam/fiber@opam:3.7.0@d70e2471", "@opam/dyn@opam:3.11.1@d3c74846",
-        "@opam/dune-rpc@opam:3.11.1@1197fefa",
-        "@opam/dune-build-info@opam:3.11.1@0dfbdab2",
+        "@opam/fiber@opam:3.7.0@d70e2471", "@opam/dyn@opam:3.12.1@7b80464e",
+        "@opam/dune-rpc@opam:3.12.1@03e71e5d",
+        "@opam/dune-build-info@opam:3.12.1@ce69ef3d",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/csexp@opam:1.5.2@46614bf4"
       ]
     },
@@ -2684,7 +2684,7 @@
       "overrides": [],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/ocplib-endian@opam:1.2@008dc942",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/cppo@opam:1.6.9@db929a12",
         "@opam/base-unix@opam:base@87d0b2eb",
         "@opam/base-threads@opam:base@36803084",
@@ -2692,7 +2692,7 @@
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/ocplib-endian@opam:1.2@008dc942",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
@@ -2778,14 +2778,14 @@
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/stdio@opam:v0.14.0@a5affb43",
         "@opam/ppx_assert@opam:v0.14.0@f5d6cf6a",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/base@opam:v0.14.3@b3ddb868",
         "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/stdio@opam:v0.14.0@a5affb43",
         "@opam/ppx_assert@opam:v0.14.0@f5d6cf6a",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@opam/base@opam:v0.14.3@b3ddb868"
       ]
     },
@@ -2814,8 +2814,8 @@
         "ocaml@4.14.1000@d41d8cd9", "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
-    "@opam/gen@opam:1.1@059b2731": {
-      "id": "@opam/gen@opam:1.1@059b2731",
+    "@opam/gen@opam:1.1@55327887": {
+      "id": "@opam/gen@opam:1.1@55327887",
       "name": "@opam/gen",
       "version": "opam:1.1",
       "source": {
@@ -2990,13 +2990,13 @@
       },
       "overrides": [],
       "dependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/stdune@opam:3.11.1@9a840882",
-        "@opam/dyn@opam:3.11.1@d3c74846", "@opam/dune@opam:3.8.3@ff88b4c5",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/stdune@opam:3.12.1@2a177cb9",
+        "@opam/dyn@opam:3.12.1@7b80464e", "@opam/dune@opam:3.8.3@ff88b4c5",
         "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/stdune@opam:3.11.1@9a840882",
-        "@opam/dyn@opam:3.11.1@d3c74846", "@opam/dune@opam:3.8.3@ff88b4c5"
+        "ocaml@4.14.1000@d41d8cd9", "@opam/stdune@opam:3.12.1@2a177cb9",
+        "@opam/dyn@opam:3.12.1@7b80464e", "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
     "@opam/either@opam:1.0.0@be5a1416": {
@@ -3021,80 +3021,80 @@
       ],
       "devDependencies": [ "@opam/dune@opam:3.8.3@ff88b4c5" ]
     },
-    "@opam/dyn@opam:3.11.1@d3c74846": {
-      "id": "@opam/dyn@opam:3.11.1@d3c74846",
+    "@opam/dyn@opam:3.12.1@7b80464e": {
+      "id": "@opam/dyn@opam:3.12.1@7b80464e",
       "name": "@opam/dyn",
-      "version": "opam:3.11.1",
+      "version": "opam:3.12.1",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/86/866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71",
-          "archive:https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
+          "archive:https://opam.ocaml.org/cache/sha256/b9/b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f",
+          "archive:https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
         ],
         "opam": {
           "name": "dyn",
-          "version": "3.11.1",
-          "path": "esy.lock/opam/dyn.3.11.1"
+          "version": "3.12.1",
+          "path": "esy.lock/opam/dyn.3.12.1"
         }
       },
       "overrides": [],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/pp@opam:1.2.0@16430027",
-        "@opam/ordering@opam:3.11.1@92c57daa",
+        "@opam/ordering@opam:3.12.1@9f3171ff",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/pp@opam:1.2.0@16430027",
-        "@opam/ordering@opam:3.11.1@92c57daa",
+        "@opam/ordering@opam:3.12.1@9f3171ff",
         "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
-    "@opam/dune-rpc@opam:3.11.1@1197fefa": {
-      "id": "@opam/dune-rpc@opam:3.11.1@1197fefa",
+    "@opam/dune-rpc@opam:3.12.1@03e71e5d": {
+      "id": "@opam/dune-rpc@opam:3.12.1@03e71e5d",
       "name": "@opam/dune-rpc",
-      "version": "opam:3.11.1",
+      "version": "opam:3.12.1",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/86/866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71",
-          "archive:https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
+          "archive:https://opam.ocaml.org/cache/sha256/b9/b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f",
+          "archive:https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
         ],
         "opam": {
           "name": "dune-rpc",
-          "version": "3.11.1",
-          "path": "esy.lock/opam/dune-rpc.3.11.1"
+          "version": "3.12.1",
+          "path": "esy.lock/opam/dune-rpc.3.12.1"
         }
       },
       "overrides": [],
       "dependencies": [
-        "@opam/xdg@opam:3.11.1@1e207b0b",
-        "@opam/stdune@opam:3.11.1@9a840882", "@opam/pp@opam:1.2.0@16430027",
-        "@opam/ordering@opam:3.11.1@92c57daa",
-        "@opam/dyn@opam:3.11.1@d3c74846", "@opam/dune@opam:3.8.3@ff88b4c5",
+        "@opam/xdg@opam:3.12.1@36e9c532",
+        "@opam/stdune@opam:3.12.1@2a177cb9", "@opam/pp@opam:1.2.0@16430027",
+        "@opam/ordering@opam:3.12.1@9f3171ff",
+        "@opam/dyn@opam:3.12.1@7b80464e", "@opam/dune@opam:3.8.3@ff88b4c5",
         "@opam/csexp@opam:1.5.2@46614bf4", "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
-        "@opam/xdg@opam:3.11.1@1e207b0b",
-        "@opam/stdune@opam:3.11.1@9a840882", "@opam/pp@opam:1.2.0@16430027",
-        "@opam/ordering@opam:3.11.1@92c57daa",
-        "@opam/dyn@opam:3.11.1@d3c74846", "@opam/dune@opam:3.8.3@ff88b4c5",
+        "@opam/xdg@opam:3.12.1@36e9c532",
+        "@opam/stdune@opam:3.12.1@2a177cb9", "@opam/pp@opam:1.2.0@16430027",
+        "@opam/ordering@opam:3.12.1@9f3171ff",
+        "@opam/dyn@opam:3.12.1@7b80464e", "@opam/dune@opam:3.8.3@ff88b4c5",
         "@opam/csexp@opam:1.5.2@46614bf4"
       ]
     },
-    "@opam/dune-configurator@opam:3.11.1@24d75a5c": {
-      "id": "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+    "@opam/dune-configurator@opam:3.12.1@13f69e99": {
+      "id": "@opam/dune-configurator@opam:3.12.1@13f69e99",
       "name": "@opam/dune-configurator",
-      "version": "opam:3.11.1",
+      "version": "opam:3.12.1",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/86/866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71",
-          "archive:https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
+          "archive:https://opam.ocaml.org/cache/sha256/b9/b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f",
+          "archive:https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
         ],
         "opam": {
           "name": "dune-configurator",
-          "version": "3.11.1",
-          "path": "esy.lock/opam/dune-configurator.3.11.1"
+          "version": "3.12.1",
+          "path": "esy.lock/opam/dune-configurator.3.12.1"
         }
       },
       "overrides": [],
@@ -3110,20 +3110,20 @@
         "@opam/base-unix@opam:base@87d0b2eb"
       ]
     },
-    "@opam/dune-build-info@opam:3.11.1@0dfbdab2": {
-      "id": "@opam/dune-build-info@opam:3.11.1@0dfbdab2",
+    "@opam/dune-build-info@opam:3.12.1@ce69ef3d": {
+      "id": "@opam/dune-build-info@opam:3.12.1@ce69ef3d",
       "name": "@opam/dune-build-info",
-      "version": "opam:3.11.1",
+      "version": "opam:3.12.1",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://opam.ocaml.org/cache/sha256/86/866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71",
-          "archive:https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz#sha256:866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
+          "archive:https://opam.ocaml.org/cache/sha256/b9/b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f",
+          "archive:https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz#sha256:b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
         ],
         "opam": {
           "name": "dune-build-info",
-          "version": "3.11.1",
-          "path": "esy.lock/opam/dune-build-info.3.11.1"
+          "version": "3.12.1",
+          "path": "esy.lock/opam/dune-build-info.3.12.1"
         }
       },
       "overrides": [],
@@ -3180,7 +3180,7 @@
       },
       "overrides": [],
       "dependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.1@ad5e299c",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.2@9fd14300",
         "@opam/react@opam:1.2.2@e0f4480e",
         "@opam/ppx_here@opam:v0.14.0@c05577d4",
         "@opam/ppx_expect@opam:v0.14.2@b6279606",
@@ -3194,7 +3194,7 @@
         "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
-        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.1@ad5e299c",
+        "ocaml@4.14.1000@d41d8cd9", "@opam/yojson@opam:2.1.2@9fd14300",
         "@opam/react@opam:1.2.2@e0f4480e",
         "@opam/ppx_here@opam:v0.14.0@c05577d4",
         "@opam/ppx_expect@opam:v0.14.2@b6279606",
@@ -3426,12 +3426,12 @@
       "overrides": [],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
@@ -3556,12 +3556,12 @@
       "overrides": [],
       "dependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/sexplib0@opam:v0.14.0@70ace5c1",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5", "@esy-ocaml/substs@0.0.1@d41d8cd9"
       ],
       "devDependencies": [
         "ocaml@4.14.1000@d41d8cd9", "@opam/sexplib0@opam:v0.14.0@70ace5c1",
-        "@opam/dune-configurator@opam:3.11.1@24d75a5c",
+        "@opam/dune-configurator@opam:3.12.1@13f69e99",
         "@opam/dune@opam:3.8.3@ff88b4c5"
       ]
     },
@@ -3700,14 +3700,14 @@
       "dependencies": [],
       "devDependencies": []
     },
-    "@babel/runtime@7.23.2@d41d8cd9": {
-      "id": "@babel/runtime@7.23.2@d41d8cd9",
+    "@babel/runtime@7.23.5@d41d8cd9": {
+      "id": "@babel/runtime@7.23.5@d41d8cd9",
       "name": "@babel/runtime",
-      "version": "7.23.2",
+      "version": "7.23.5",
       "source": {
         "type": "install",
         "source": [
-          "archive:https://registry.npmjs.org/@babel/runtime/-/runtime-7.23.2.tgz#sha1:062b0ac103261d68a966c4c7baf2ae3e62ec3885"
+          "archive:https://registry.npmjs.org/@babel/runtime/-/runtime-7.23.5.tgz#sha1:11edb98f8aeec529b82b211028177679144242db"
         ]
       },
       "overrides": [],
diff --git a/esy.lock/opam/dune-build-info.3.11.1/opam b/esy.lock/opam/dune-build-info.3.12.1/opam
similarity index 75%
rename from esy.lock/opam/dune-build-info.3.11.1/opam
rename to esy.lock/opam/dune-build-info.3.12.1/opam
index f0bb6ed48..9bf95f7bf 100644
--- a/esy.lock/opam/dune-build-info.3.11.1/opam
+++ b/esy.lock/opam/dune-build-info.3.12.1/opam
@@ -37,10 +37,10 @@ build: [
 ]
 url {
   src:
-    "https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz"
+    "https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz"
   checksum: [
-    "sha256=866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
-    "sha512=c888153b204a16bcfed2636de776bbd5f9ca84484e716cc1e9ef3ba3c904e9dd15a2609ae943cddb6097912623ec54618c58386d6730ff742d746850400fb3cc"
+    "sha256=b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
+    "sha512=1a4159d18a7aee0ca9f53f176955a41f5a6d83b16885e7f6ac47326453572df74a87f21f4ceddb8d2e94e00f61d2ba5ca6dba299679968f1d151d2811dcd2014"
   ]
 }
-x-commit-hash: "7cbb0e7277c6cacd1ccf7941cac5a03c25fc63cf"
+x-commit-hash: "2e4994f005e9a94993150601bdb60759d9de5ab6"
diff --git a/esy.lock/opam/dune-configurator.3.11.1/opam b/esy.lock/opam/dune-configurator.3.12.1/opam
similarity index 75%
rename from esy.lock/opam/dune-configurator.3.11.1/opam
rename to esy.lock/opam/dune-configurator.3.12.1/opam
index 8ee593d15..9d8e8e421 100644
--- a/esy.lock/opam/dune-configurator.3.11.1/opam
+++ b/esy.lock/opam/dune-configurator.3.12.1/opam
@@ -41,10 +41,10 @@ build: [
 ]
 url {
   src:
-    "https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz"
+    "https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz"
   checksum: [
-    "sha256=866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
-    "sha512=c888153b204a16bcfed2636de776bbd5f9ca84484e716cc1e9ef3ba3c904e9dd15a2609ae943cddb6097912623ec54618c58386d6730ff742d746850400fb3cc"
+    "sha256=b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
+    "sha512=1a4159d18a7aee0ca9f53f176955a41f5a6d83b16885e7f6ac47326453572df74a87f21f4ceddb8d2e94e00f61d2ba5ca6dba299679968f1d151d2811dcd2014"
   ]
 }
-x-commit-hash: "7cbb0e7277c6cacd1ccf7941cac5a03c25fc63cf"
+x-commit-hash: "2e4994f005e9a94993150601bdb60759d9de5ab6"
diff --git a/esy.lock/opam/dune-rpc.3.11.1/opam b/esy.lock/opam/dune-rpc.3.12.1/opam
similarity index 69%
rename from esy.lock/opam/dune-rpc.3.11.1/opam
rename to esy.lock/opam/dune-rpc.3.12.1/opam
index 9ec698147..c8f2982e9 100644
--- a/esy.lock/opam/dune-rpc.3.11.1/opam
+++ b/esy.lock/opam/dune-rpc.3.12.1/opam
@@ -35,10 +35,10 @@ build: [
 ]
 url {
   src:
-    "https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz"
+    "https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz"
   checksum: [
-    "sha256=866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
-    "sha512=c888153b204a16bcfed2636de776bbd5f9ca84484e716cc1e9ef3ba3c904e9dd15a2609ae943cddb6097912623ec54618c58386d6730ff742d746850400fb3cc"
+    "sha256=b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
+    "sha512=1a4159d18a7aee0ca9f53f176955a41f5a6d83b16885e7f6ac47326453572df74a87f21f4ceddb8d2e94e00f61d2ba5ca6dba299679968f1d151d2811dcd2014"
   ]
 }
-x-commit-hash: "7cbb0e7277c6cacd1ccf7941cac5a03c25fc63cf"
+x-commit-hash: "2e4994f005e9a94993150601bdb60759d9de5ab6"
diff --git a/esy.lock/opam/dyn.3.11.1/opam b/esy.lock/opam/dyn.3.12.1/opam
similarity index 67%
rename from esy.lock/opam/dyn.3.11.1/opam
rename to esy.lock/opam/dyn.3.12.1/opam
index 30ca00c80..797f82d4a 100644
--- a/esy.lock/opam/dyn.3.11.1/opam
+++ b/esy.lock/opam/dyn.3.12.1/opam
@@ -32,10 +32,10 @@ build: [
 ]
 url {
   src:
-    "https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz"
+    "https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz"
   checksum: [
-    "sha256=866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
-    "sha512=c888153b204a16bcfed2636de776bbd5f9ca84484e716cc1e9ef3ba3c904e9dd15a2609ae943cddb6097912623ec54618c58386d6730ff742d746850400fb3cc"
+    "sha256=b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
+    "sha512=1a4159d18a7aee0ca9f53f176955a41f5a6d83b16885e7f6ac47326453572df74a87f21f4ceddb8d2e94e00f61d2ba5ca6dba299679968f1d151d2811dcd2014"
   ]
 }
-x-commit-hash: "7cbb0e7277c6cacd1ccf7941cac5a03c25fc63cf"
+x-commit-hash: "2e4994f005e9a94993150601bdb60759d9de5ab6"
diff --git a/esy.lock/opam/gen.1.1/opam b/esy.lock/opam/gen.1.1/opam
index 30e8e332f..cf9ae07c7 100644
--- a/esy.lock/opam/gen.1.1/opam
+++ b/esy.lock/opam/gen.1.1/opam
@@ -11,7 +11,7 @@ depends: [
   "dune" {>= "1.1"}
   "seq"
   "odoc" {with-doc}
-  "qcheck" {with-test}
+  "qcheck" {with-test & >= "0.9"}
   "qtest" {with-test}
   "ounit2" {with-test}
   "ocaml" { >= "4.03.0" }
diff --git a/esy.lock/opam/odoc.2.2.1/opam b/esy.lock/opam/odoc.2.2.2/opam
similarity index 79%
rename from esy.lock/opam/odoc.2.2.1/opam
rename to esy.lock/opam/odoc.2.2.2/opam
index 03d20c693..54f4b2d87 100644
--- a/esy.lock/opam/odoc.2.2.1/opam
+++ b/esy.lock/opam/odoc.2.2.2/opam
@@ -52,10 +52,10 @@ build: [
   ["dune" "build" "-p" name "-j" jobs]
 ]
 url {
-  src: "https://github.com/ocaml/odoc/releases/download/2.2.1/odoc-2.2.1.tbz"
+  src: "https://github.com/ocaml/odoc/releases/download/2.2.2/odoc-2.2.2.tbz"
   checksum: [
-    "sha256=1786e53bf0824fe1c7c7b81d2a7d846846a5d11677969e6396361f77a3816803"
-    "sha512=044e37eb3dcc77d9cc8124be558cce77a438723b90225273fb3401d3315c57c8c2f395a48ebd1b6aacc01b00cbfa4bd0be1923d2bd9bd3cc92d0604eadaabc4f"
+    "sha256=6ec331a1da22ec8b8feca73d4b8b6269043f4b36b10dd49f557f42449633672b"
+    "sha512=5bf48555f84d17f61e58cad16703e47c07effde44d1e232f7f227c638f51d57a3d8ec2e71804876c8fbf1035384478e79382d8bdc5a271ea599e42c9cd1d6ab2"
   ]
 }
-x-commit-hash: "2d8a6776c19ffa995ae285cd1dfc27f2fea3820a"
+x-commit-hash: "34a48e2543f6ea5716e9ee922954fa0917561dd7"
diff --git a/esy.lock/opam/ordering.3.11.1/opam b/esy.lock/opam/ordering.3.12.1/opam
similarity index 66%
rename from esy.lock/opam/ordering.3.11.1/opam
rename to esy.lock/opam/ordering.3.12.1/opam
index 5416c8078..f4b714be7 100644
--- a/esy.lock/opam/ordering.3.11.1/opam
+++ b/esy.lock/opam/ordering.3.12.1/opam
@@ -30,10 +30,10 @@ build: [
 ]
 url {
   src:
-    "https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz"
+    "https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz"
   checksum: [
-    "sha256=866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
-    "sha512=c888153b204a16bcfed2636de776bbd5f9ca84484e716cc1e9ef3ba3c904e9dd15a2609ae943cddb6097912623ec54618c58386d6730ff742d746850400fb3cc"
+    "sha256=b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
+    "sha512=1a4159d18a7aee0ca9f53f176955a41f5a6d83b16885e7f6ac47326453572df74a87f21f4ceddb8d2e94e00f61d2ba5ca6dba299679968f1d151d2811dcd2014"
   ]
 }
-x-commit-hash: "7cbb0e7277c6cacd1ccf7941cac5a03c25fc63cf"
+x-commit-hash: "2e4994f005e9a94993150601bdb60759d9de5ab6"
diff --git a/esy.lock/opam/stdune.3.11.1/opam b/esy.lock/opam/stdune.3.12.1/opam
similarity index 71%
rename from esy.lock/opam/stdune.3.11.1/opam
rename to esy.lock/opam/stdune.3.12.1/opam
index 2dfc92539..00670e651 100644
--- a/esy.lock/opam/stdune.3.11.1/opam
+++ b/esy.lock/opam/stdune.3.12.1/opam
@@ -36,10 +36,10 @@ build: [
 ]
 url {
   src:
-    "https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz"
+    "https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz"
   checksum: [
-    "sha256=866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
-    "sha512=c888153b204a16bcfed2636de776bbd5f9ca84484e716cc1e9ef3ba3c904e9dd15a2609ae943cddb6097912623ec54618c58386d6730ff742d746850400fb3cc"
+    "sha256=b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
+    "sha512=1a4159d18a7aee0ca9f53f176955a41f5a6d83b16885e7f6ac47326453572df74a87f21f4ceddb8d2e94e00f61d2ba5ca6dba299679968f1d151d2811dcd2014"
   ]
 }
-x-commit-hash: "7cbb0e7277c6cacd1ccf7941cac5a03c25fc63cf"
+x-commit-hash: "2e4994f005e9a94993150601bdb60759d9de5ab6"
diff --git a/esy.lock/opam/xdg.3.11.1/opam b/esy.lock/opam/xdg.3.12.1/opam
similarity index 68%
rename from esy.lock/opam/xdg.3.11.1/opam
rename to esy.lock/opam/xdg.3.12.1/opam
index 9a6a17d03..36980d28f 100644
--- a/esy.lock/opam/xdg.3.11.1/opam
+++ b/esy.lock/opam/xdg.3.12.1/opam
@@ -31,10 +31,10 @@ build: [
 ]
 url {
   src:
-    "https://github.com/ocaml/dune/releases/download/3.11.1/dune-3.11.1.tbz"
+    "https://github.com/ocaml/dune/releases/download/3.12.1/dune-3.12.1.tbz"
   checksum: [
-    "sha256=866f2307adadaf7604f3bf9d98bb4098792baa046953a6726c96c40fc5ed3f71"
-    "sha512=c888153b204a16bcfed2636de776bbd5f9ca84484e716cc1e9ef3ba3c904e9dd15a2609ae943cddb6097912623ec54618c58386d6730ff742d746850400fb3cc"
+    "sha256=b9fd6560879f9d340ae8a87c967b0d2bcd3c4120cffcd9fb661f325078f74f6f"
+    "sha512=1a4159d18a7aee0ca9f53f176955a41f5a6d83b16885e7f6ac47326453572df74a87f21f4ceddb8d2e94e00f61d2ba5ca6dba299679968f1d151d2811dcd2014"
   ]
 }
-x-commit-hash: "7cbb0e7277c6cacd1ccf7941cac5a03c25fc63cf"
+x-commit-hash: "2e4994f005e9a94993150601bdb60759d9de5ab6"
diff --git a/esy.lock/opam/yojson.2.1.1/opam b/esy.lock/opam/yojson.2.1.2/opam
similarity index 77%
rename from esy.lock/opam/yojson.2.1.1/opam
rename to esy.lock/opam/yojson.2.1.2/opam
index 0703d53bf..df37a739d 100644
--- a/esy.lock/opam/yojson.2.1.1/opam
+++ b/esy.lock/opam/yojson.2.1.2/opam
@@ -39,10 +39,10 @@ build: [
 dev-repo: "git+https://github.com/ocaml-community/yojson.git"
 url {
   src:
-    "https://github.com/ocaml-community/yojson/releases/download/2.1.1/yojson-2.1.1.tbz"
+    "https://github.com/ocaml-community/yojson/releases/download/2.1.2/yojson-2.1.2.tbz"
   checksum: [
-    "sha256=d58183207b198dc065866239066e074c34f9e139c0d9c4175a38809790e88173"
-    "sha512=f7b8529900acb29bc6236d8312d3ebcadbcb3f9d361c8acaed9f7fc7e30527b41a1f3cff80382dde445e6da18a4edc5a9c6758af24affce1022d0741dbd9daeb"
+    "sha256=59f2f1abbfc8a7ccbdbf608894e5c75e8a76006e34899254446f83e200dfb4f9"
+    "sha512=309cba7568dec51de20c7ab8df033258c275b8d58b0a36a66b26e673a3bc050cbd7e39ff8fe4796e89263e125bcc21e04dc36a394f3cc201956887eee1fb281a"
   ]
 }
-x-commit-hash: "57bc8ca0eaf5bdb423fcdece49ea0d1c2866f90c"
+x-commit-hash: "e51163ee04ad79408975545ec5fc3b7dc41f68eb"
diff --git a/esy.lock/overrides/ee5be9c1213cfc9c8d43f4061c829e80/package.json b/esy.lock/overrides/44ff3c39826df68739c4470881a91b5f/package.json
similarity index 95%
rename from esy.lock/overrides/ee5be9c1213cfc9c8d43f4061c829e80/package.json
rename to esy.lock/overrides/44ff3c39826df68739c4470881a91b5f/package.json
index a22a717ab..74d697e21 100644
--- a/esy.lock/overrides/ee5be9c1213cfc9c8d43f4061c829e80/package.json
+++ b/esy.lock/overrides/44ff3c39826df68739c4470881a91b5f/package.json
@@ -2,7 +2,7 @@
   "name": "esy-z3",
   "version": "4.8.12000",
   "description": "z3 packaged for esy",
-  "source": "https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.2.tar.gz#md5:4061317f7948c19abd13041c5a32b057",
+  "source": "https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.12.3.tar.gz#md5:a18ea8cc1ba59d87a6ea966227732038",
   "override": {
     "exportedEnv": {
       "DYLD_LIBRARY_PATH": {
@@ -50,4 +50,4 @@
       "ocaml": ">=4.3.0"
     }
   }
-}
\ No newline at end of file
+}
diff --git a/wisl/lib/ParserAndCompiler/WAnnot.ml b/wisl/lib/ParserAndCompiler/WAnnot.ml
index ad8f80358..7649048fe 100644
--- a/wisl/lib/ParserAndCompiler/WAnnot.ml
+++ b/wisl/lib/ParserAndCompiler/WAnnot.ml
@@ -1,36 +1,50 @@
 type nest_kind =
-  | NoNest  (** This command doesn't contain a nest *)
   | LoopBody of string
       (** This command nests its loop body an (abstracted) function call *)
   | FunCall of string  (** This command nests the body of a function call *)
 [@@deriving yojson]
 
-type stmt_end_kind = NotEnd | EndNormal | EndWithBranch of WBranchCase.t
-[@@deriving yojson]
-
 (** How does this command map to a WISL statment? *)
 type stmt_kind =
-  | Single  (** A command that maps one-to-one with a WISL statement *)
-  | LoopPrefix  (** A command in the prefix of a loop body function *)
-  | Multi of stmt_end_kind
+  | Normal of bool
       (** A command that makes up part of a WISL statement, and whether this is the last cmd of said statement *)
-[@@deriving yojson]
+  | Return of bool
+      (** Same as [Normal], but specific to the return statement *)
+  | Hidden  (** A command that doesn't map to a particular WISL statement *)
+  | LoopPrefix  (** A command in the prefix of a loop body function *)
+[@@deriving yojson, show]
 
 type t = {
   origin_loc : Gil_syntax.Location.t option;
       (** Better not to know what this is for *)
   origin_id : int option;  (** Origin Id, that should be abstracted away *)
   loop_info : string list;
-  stmt_kind : stmt_kind; [@default Single]
-  nest_kind : nest_kind; [@default NoNest]
-  is_hidden : bool; [@default false]
-      (** Should this command be hidden when debugging? *)
-  is_return : bool; [@default false]
+  stmt_kind : stmt_kind; [@default Normal true]
+  branch_kind : WBranchCase.kind option;
+  nest_kind : nest_kind option;
 }
 [@@deriving yojson, make]
 
-let make_basic ?origin_loc ?loop_info () = make ?origin_loc ?loop_info ()
+let make_multi
+    ?origin_loc
+    ?origin_id
+    ?loop_info
+    ?nest_kind
+    ?(is_return = false)
+    () =
+  let make = make ?origin_loc ?origin_id ?loop_info ?nest_kind in
+  if is_return then
+    (make ~stmt_kind:(Return false) (), make ~stmt_kind:(Return true) ())
+  else (make ~stmt_kind:(Normal false) (), make ~stmt_kind:(Normal true) ())
+
+let make_basic ?origin_loc ?loop_info () =
+  make ~stmt_kind:Hidden ?origin_loc ?loop_info ()
+
 let get_origin_loc { origin_loc; _ } = origin_loc
 let get_loop_info { loop_info; _ } = loop_info
 let set_loop_info loop_info annot = { annot with loop_info }
-let is_hidden { is_hidden; _ } = is_hidden
+
+let is_hidden { stmt_kind; _ } =
+  match stmt_kind with
+  | Hidden -> true
+  | _ -> false
diff --git a/wisl/lib/ParserAndCompiler/wisl2Gil.ml b/wisl/lib/ParserAndCompiler/wisl2Gil.ml
index 34881b1f0..604db1a57 100644
--- a/wisl/lib/ParserAndCompiler/wisl2Gil.ml
+++ b/wisl/lib/ParserAndCompiler/wisl2Gil.ml
@@ -92,7 +92,7 @@ let rec compile_expr ?(fname = "main") ?(is_loop_prefix = false) expr :
       | PLUS | MINUS | LESSEQUAL | LESSTHAN | GREATEREQUAL | GREATERTHAN -> true
       | _ -> false)
   in
-  let stmt_kind = if is_loop_prefix then WAnnot.LoopPrefix else WAnnot.Single in
+  let stmt_kind = if is_loop_prefix then Some WAnnot.LoopPrefix else None in
   let open WExpr in
   match get expr with
   | Val v -> ([], Expr.Lit (compile_val v))
@@ -128,7 +128,7 @@ let rec compile_expr ?(fname = "main") ?(is_loop_prefix = false) expr :
         @ [
             ( WAnnot.make ~origin_id:(get_id expr)
                 ~origin_loc:(CodeLoc.to_location (get_loc expr))
-                ~stmt_kind (),
+                ?stmt_kind (),
               None,
               call_i_plus );
           ],
@@ -590,19 +590,21 @@ let compile_inv_and_while ~fname ~while_stmt ~invariant =
   let annot_while =
     WAnnot.make ~origin_id:(WStmt.get_id while_stmt)
       ~origin_loc:(CodeLoc.to_location while_loc)
-      ~stmt_kind:(Multi NotEnd) ()
+      ~stmt_kind:(Normal false) ()
   in
   let rec map_reassign_vars acc = function
     | cmd :: rest ->
         let annot_while =
           match rest with
-          | [] -> { annot_while with stmt_kind = Multi EndNormal }
+          | [] -> { annot_while with stmt_kind = Normal true }
           | _ -> annot_while
         in
         map_reassign_vars ((annot_while, None, cmd) :: acc) rest
     | [] -> List.rev acc
   in
-  let annot_call_while = { annot_while with nest_kind = LoopBody loop_fname } in
+  let annot_call_while =
+    { annot_while with nest_kind = Some (LoopBody loop_fname) }
+  in
   let lab_cmds =
     (annot_call_while, None, call_cmd) :: map_reassign_vars [] reassign_vars
   in
@@ -652,7 +654,7 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl =
         WAnnot.make ~origin_id:sid_while ~origin_loc:(CodeLoc.to_location sloc)
           ()
       in
-      let annot_hidden = WAnnot.{ annot with is_hidden = true } in
+      let annot_hidden = WAnnot.{ annot with stmt_kind = Hidden } in
       let headlabopt = Some looplab in
       let headcmd = Cmd.Skip in
       let headcmd_lab = (annot_hidden, headlabopt, headcmd) in
@@ -696,10 +698,8 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl =
   | { snode = Dispose e; sid; sloc } :: rest ->
       let cmdle, comp_e = compile_expr e in
       let annot, annot_final =
-        let mk =
-          WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc)
-        in
-        (mk ~stmt_kind:(Multi NotEnd) (), mk ~stmt_kind:(Multi EndNormal) ())
+        WAnnot.make_multi ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc)
+          ()
       in
       let faillab, ctnlab = (gen_str fail_lab, gen_str ctn_lab) in
       let testcmd =
@@ -729,10 +729,8 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl =
   | { snode = Lookup (x, e); sid; sloc } :: rest ->
       let cmdle, comp_e = compile_expr e in
       let annot, annot_final =
-        let mk =
-          WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc)
-        in
-        (mk ~stmt_kind:(Multi NotEnd) (), mk ~stmt_kind:(Multi EndNormal) ())
+        WAnnot.make_multi ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc)
+          ()
       in
       let v_get = gen_str gvar in
       let faillab, ctnlab = (gen_str fail_lab, gen_str ctn_lab) in
@@ -769,10 +767,8 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl =
   (* Property Update *)
   | { snode = Update (e1, e2); sid; sloc } :: rest ->
       let get_annot, set_annot =
-        let mk =
-          WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc)
-        in
-        (mk ~stmt_kind:(Multi NotEnd) (), mk ~stmt_kind:(Multi EndNormal) ())
+        WAnnot.make_multi ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc)
+          ()
       in
       let cmdle1, comp_e1 = compile_expr e1 in
       let cmdle2, comp_e2 = compile_expr e2 in
@@ -834,12 +830,13 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl =
       let annot =
         WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc) ()
       in
-      let annot_hidden = { annot with is_hidden = true } in
+      let annot_hidden = { annot with stmt_kind = Hidden } in
       let annot_prefix =
         let stmt_kind =
-          WAnnot.(if is_loop_prefix then LoopPrefix else Single)
+          WAnnot.(if is_loop_prefix then LoopPrefix else Normal true)
         in
-        { annot with stmt_kind }
+        let branch_kind = Some WBranchCase.IfElseKind in
+        { annot with stmt_kind; branch_kind }
       in
       let cmdle, guard = compile_expr e in
       let comp_sl1, new_functions1 = compile_list sl1 in
@@ -967,12 +964,9 @@ let rec compile_function
   in
   let cmdle, comp_ret_expr = compile_expr ~fname:name return_expr in
   let ret_annot, final_ret_annot =
-    let mk =
-      WAnnot.make
-        ~origin_loc:(CodeLoc.to_location (WExpr.get_loc return_expr))
-        ~origin_id:(WExpr.get_id return_expr) ~is_return:true
-    in
-    (mk ~stmt_kind:(Multi NotEnd) (), mk ~stmt_kind:(Multi EndNormal) ())
+    WAnnot.make_multi
+      ~origin_loc:(CodeLoc.to_location (WExpr.get_loc return_expr))
+      ~origin_id:(WExpr.get_id return_expr) ~is_return:true ()
   in
   let retassigncmds =
     cmdle
diff --git a/wisl/lib/debugging/wislLifter.ml b/wisl/lib/debugging/wislLifter.ml
index 15199e659..cd767e00d 100644
--- a/wisl/lib/debugging/wislLifter.ml
+++ b/wisl/lib/debugging/wislLifter.ml
@@ -6,10 +6,13 @@ module DL = Debugger_log
 module Exec_map = Debugger.Utils.Exec_map
 module Unify_map = Debugger.Utils.Unify_map
 open Syntaxes.Option
-module Ext_list = Utils.Ext_list
+open Syntaxes.Result_of_option
+open Utils
 module Annot = WParserAndCompiler.Annot
+module Gil_branch_case = Gil_syntax.Branch_case
+module Branch_case = WBranchCase
 open Annot
-open WBranchCase
+open Branch_case
 open Debugger.Lifter
 
 type rid = L.Report_id.t [@@deriving yojson, show]
@@ -22,6 +25,9 @@ let rec int_to_letters = function
       let char = Char.chr (65 + remainder) |> Char.escaped in
       char ^ int_to_letters (i / 26)
 
+let ( let++ ) f o = Result.map o f
+let ( let** ) o f = Result.bind o f
+
 module Make
     (Gil : Gillian.Debugger.Lifter.Gil_fallback_lifter.Gil_lifter_with_state)
     (Verification : Engine.Verifier.S with type annot = Annot.t) =
@@ -37,18 +43,15 @@ struct
   module Gil_lifter = Gil.Lifter
 
   type cmd_report = CmdReport.t [@@deriving yojson]
-  type branch_case = WBranchCase.t [@@deriving yojson]
-  type branch_data = rid * BranchCase.t option [@@deriving yojson]
+  type branch_data = rid * Gil_branch_case.t option [@@deriving yojson]
   type exec_data = cmd_report executed_cmd_data [@@deriving yojson]
-  type stack_direction = In | Out of rid
+  type stack_direction = In | Out of rid [@@deriving yojson]
 
   let annot_to_wisl_stmt annot wisl_ast =
     let origin_id = annot.origin_id in
     let wprog = WProg.get_by_id wisl_ast origin_id in
     match wprog with
-    | `WStmt wstmt ->
-        DL.log (fun m -> m "WISL STMT: %a" WStmt.pp wstmt);
-        Some wstmt.snode
+    | `WStmt wstmt -> Some wstmt.snode
     | _ -> None
 
   let get_origin_node_str wisl_ast origin_id =
@@ -73,192 +76,396 @@ struct
             failwith "get_fun_call_name: function name wasn't a literal expr!")
     | _ -> None
 
-  type map = (branch_case, cmd_data, branch_data) Exec_map.t
+  type map = (Branch_case.t, cmd_data, branch_data) Exec_map.t
 
   and cmd_data = {
-    ids : rid list;
+    id : rid;
+    all_ids : rid list;
     display : string;
     unifys : unification list;
     errors : string list;
     mutable submap : map submap;
-    gil_branch_path : BranchCase.path;
-    branch_path : branch_case list;
-    parent : parent; [@to_yojson fun _ -> `Null]
+    (* branch_path : Branch_case.t list; *)
+    prev : (rid * Branch_case.t option) option;
     callers : rid list;
     func_return_label : (string * int) option;
   }
-
-  and parent = (map * (branch_data * branch_case) option) option
   [@@deriving yojson]
 
-  module PartialCmds = struct
+  module Partial_cmds = struct
+    type prev = rid * Branch_case.t option * rid list [@@deriving yojson]
+
     type partial_data = {
-      display : string;
-      ids : rid Ext_list.t;
-      errors : string Ext_list.t;
-      mutable submap : map submap;
-      mutable inner_path : branch_data list;
+      prev : prev option;
+      all_ids : (rid * (Branch_case.kind option * Branch_case.case)) Ext_list.t;
+      unexplored_paths : (rid * Gil_branch_case.t option) Stack.t;
+      ends : (Branch_case.case * branch_data) Ext_list.t;
+      mutable id : rid option;
+      mutable display : string option;
+      mutable stack_info : (rid list * stack_direction option) option;
+      mutable nest_kind : nest_kind option;
       unifys : unification Ext_list.t;
-      unexplored_paths : branch_data list Stack.t;
-      out_paths : (branch_case * branch_data list) Ext_list.t;
-      mutable unknown_outs_count : int;
+      errors : string Ext_list.t;
     }
     [@@deriving to_yojson]
 
-    let make_partial_data display =
+    let init_partial ~prev =
       {
-        display;
-        ids = Ext_list.make ();
-        errors = Ext_list.make ();
-        unifys = Ext_list.make ();
-        submap = NoSubmap;
-        inner_path = [];
+        prev;
+        all_ids = Ext_list.make ();
         unexplored_paths = Stack.create ();
-        out_paths = Ext_list.make ();
-        unknown_outs_count = 0;
+        ends = Ext_list.make ();
+        id = None;
+        display = None;
+        stack_info = None;
+        nest_kind = None;
+        unifys = Ext_list.make ();
+        errors = Ext_list.make ();
       }
 
-    type t = (int, partial_data) Hashtbl.t [@@deriving to_yojson]
-
-    let update_partial_data end_kind exec_data d =
-      let { id; unifys; errors; cmd_report; _ } = exec_data in
-      let annot = CmdReport.(cmd_report.annot) in
-      d.ids |> Ext_list.append id;
-      unifys |> List.iter (fun unify -> d.unifys |> Ext_list.append unify);
-      errors |> List.iter (fun error -> d.errors |> Ext_list.append error);
-      (match exec_data.kind with
-      | Branch cases ->
-          cases
-          |> List.iter (fun (case, _) ->
-                 let path = (id, Some case) :: d.inner_path in
-                 match end_kind with
-                 | NotEnd -> d.unexplored_paths |> Stack.push path
-                 | EndNormal ->
-                     let count = d.unknown_outs_count in
-                     let case = Gil count in
-                     d.unknown_outs_count <- count + 1;
-                     d.out_paths |> Ext_list.append (case, path)
-                 | EndWithBranch _ ->
-                     failwith "EndWithBranch on branching cmd not supported!")
-      | Normal -> (
-          let path = (id, None) :: d.inner_path in
-          match end_kind with
-          | NotEnd -> ()
-          | EndNormal ->
-              let count = d.unknown_outs_count in
-              let case = Gil count in
-              d.unknown_outs_count <- count + 1;
-              d.out_paths |> Ext_list.append (case, path)
-          | EndWithBranch case -> d.out_paths |> Ext_list.append (case, path))
-      | Final -> ());
-      match (d.submap, annot.nest_kind) with
-      | _, NoNest -> ()
-      | NoSubmap, LoopBody p -> d.submap <- Proc p
-      | _, _ ->
-          DL.failwith
-            (fun () ->
-              [
-                ("annot", Annot.to_yojson annot);
-                ("exec_data", exec_data_to_yojson exec_data);
-                ("partial_data", partial_data_to_yojson d);
-              ])
-            "WislLifter.update_partial_data: multiple submaps in WISL \
-             statement!"
+    type t = (rid, partial_data) Hashtbl.t [@@deriving to_yojson]
 
-    type finished_partial_data = {
-      ids : rid list;
+    type finished = {
+      prev : (rid * Branch_case.t option) option;
+      id : rid;
+      all_ids : rid list;
       display : string;
       unifys : unification list;
       errors : string list;
-      cmd_kind : (branch_case, branch_data) cmd_kind;
+      kind : (Branch_case.t, branch_data) cmd_kind;
       submap : map submap;
+      callers : rid list;
+      stack_direction : stack_direction option;
     }
+    [@@deriving yojson]
+
+    type partial_result =
+      | Finished of finished
+      | StepAgain of (rid option * Gil_branch_case.t option)
 
-    type partial_cmd_result =
-      | Finished of finished_partial_data
-      | StepAgain of (rid option * BranchCase.t option)
+    let step_again ?id ?branch_case () = Ok (StepAgain (id, branch_case))
 
-    let make_finished_partial
-        is_final
-        { ids; display; unifys; errors; out_paths; submap; _ } =
-      let ids = ids |> Ext_list.to_list in
+    let ends_to_cases ~nest_kind (ends : (Branch_case.case * branch_data) list)
+        =
+      let- () =
+        match (nest_kind, ends) with
+        | Some (FunCall _), [ (Unknown, bdata) ] ->
+            Some (Ok [ (FuncExitPlaceholder, bdata) ])
+        | Some (FunCall _), _ ->
+            Some (Error "Unexpected branching in cmd with FunCall nest!")
+        | _ -> None
+      in
+      let counts = Hashtbl.create 0 in
+      let () =
+        ends
+        |> List.iter (fun (case_kind, _) ->
+               let total, _ =
+                 Hashtbl.find_opt counts case_kind
+                 |> Option.value ~default:(0, 0)
+               in
+               Hashtbl.replace counts case_kind (total + 1, 0))
+      in
+      ends
+      |> List.map (fun (kind, branch_data) ->
+             let total, count = Hashtbl.find counts kind in
+             let ix =
+               match (kind, total) with
+               | IfElse _, 1 -> -1
+               | _ -> count
+             in
+             let () = Hashtbl.replace counts kind (total, count + 1) in
+             (Case (kind, ix), branch_data))
+      |> Result.ok
+
+    let is_return exec_data =
+      let annot = CmdReport.(exec_data.cmd_report.annot) in
+      match annot.stmt_kind with
+      | Return _ -> true
+      | _ -> false
+
+    let finish ~is_loop_func ~proc_name ~exec_data partial =
+      let ({
+             prev;
+             all_ids;
+             id;
+             display;
+             stack_info;
+             ends;
+             nest_kind;
+             unifys;
+             errors;
+             _;
+           }
+            : partial_data) =
+        partial
+      in
+      let prev =
+        let+ id, branch, _ = prev in
+        (id, branch)
+      in
+      let** id =
+        id |> Option.to_result ~none:"Trying to finish partial with no id!"
+      in
+      let** display =
+        display
+        |> Option.to_result ~none:"Trying to finish partial with no display!"
+      in
+      let** callers, stack_direction =
+        stack_info
+        |> Option.to_result ~none:"Trying to finish partial with no stack info!"
+      in
+      let all_ids = all_ids |> Ext_list.to_list |> List.map fst in
       let unifys = unifys |> Ext_list.to_list in
       let errors = errors |> Ext_list.to_list in
-      let cmd_kind =
-        match out_paths |> Ext_list.to_list with
-        | [] | [ (_, [ (_, None) ]) ] -> if is_final then Final else Normal
-        | paths ->
+      let ends = Ext_list.to_list ends in
+      let submap =
+        match nest_kind with
+        | Some (LoopBody p) -> Proc p
+        | _ -> NoSubmap
+      in
+      let++ display, kind =
+        match ends with
+        | _ when is_return exec_data -> Ok (display, Final)
+        | [] -> Ok (display, Final)
+        | [ (Unknown, _) ] ->
+            if is_loop_func && get_fun_call_name exec_data = Some proc_name then
+              Ok ("<end of loop>", Final)
+            else Ok (display, Normal)
+        | ends ->
+            let++ cases = ends_to_cases ~nest_kind ends in
             let cases =
-              paths
-              |> List.map (fun (case, path) ->
-                     let branch_data = List.hd path in
-                     (case, branch_data))
+              List.sort (fun (a, _) (b, _) -> Branch_case.compare a b) cases
             in
-            Branch cases
-      in
-      Finished { ids; display; unifys; errors; cmd_kind; submap }
-
-    let update annot (d : partial_data) (exec_data : exec_data) :
-        partial_cmd_result =
-      let failwith s =
-        DL.failwith
-          (fun () ->
-            [
-              ("annot", Annot.to_yojson annot);
-              ("exec_data", exec_data_to_yojson exec_data);
-              ("partial_data", partial_data_to_yojson d);
-            ])
-          ("WislLifter.PartialCmds.update: " ^ s)
-      in
-      let end_kind =
-        match annot.stmt_kind with
-        | Multi b -> b
-        | _ -> failwith "tried to update partial with non-Multi cmd!"
+            (display, Branch cases)
       in
-      d |> update_partial_data end_kind exec_data;
-      let is_final, result =
-        match (exec_data.kind, end_kind) with
-        | Final, _ -> (true, None)
-        | _, EndNormal when annot.is_return -> (true, None)
-        | _, (EndNormal | EndWithBranch _) | Branch _, _ -> (false, None)
-        | Normal, _ -> (false, Some (StepAgain (None, None)))
+      Finished
+        {
+          prev;
+          all_ids;
+          id;
+          display;
+          callers;
+          stack_direction;
+          unifys;
+          errors;
+          submap;
+          kind;
+        }
+
+    module Update = struct
+      let get_is_end ({ stmt_kind; _ } : Annot.t) =
+        match stmt_kind with
+        | Normal b | Return b -> Ok b
+        | Hidden -> Ok false
+        | LoopPrefix as k ->
+            Fmt.error "%a cmd should have been skipped!" Annot.pp_stmt_kind k
+
+      let resolve_case
+          ?gil_case
+          (kind : Branch_case.kind option)
+          (prev_case : Branch_case.case) =
+        match (kind, prev_case) with
+        | None, prev_case -> Ok prev_case
+        | Some prev_kind, Unknown -> (
+            match prev_kind with
+            | IfElseKind -> (
+                match gil_case with
+                | Some (Gil_branch_case.GuardedGoto b) -> Ok (IfElse b)
+                | _ -> Error "IfElseKind expects a GuardedGoto gil case"))
+        | Some _, _ ->
+            Error "HORROR - branch kind is set with pre-existing case!"
+
+      let update_paths ~exec_data ~branch_case ~branch_kind partial =
+        let ({ id; kind; cmd_report; _ } : exec_data) = exec_data in
+        let annot = CmdReport.(cmd_report.annot) in
+        let { ends; unexplored_paths; _ } = partial in
+        let** is_end = get_is_end annot in
+        match (is_end, kind) with
+        | _, Final -> Ok ()
+        | false, Normal ->
+            Stack.push (id, None) unexplored_paths;
+            Ok ()
+        | false, Branch cases ->
+            cases
+            |> List.iter (fun (gil_case, ()) ->
+                   Stack.push (id, Some gil_case) unexplored_paths);
+            Ok ()
+        | true, Normal ->
+            Ext_list.add (branch_case, (id, None)) ends;
+            Ok ()
+        | true, Branch cases ->
+            cases
+            |> List_utils.iter_results (fun (gil_case, ()) ->
+                   let++ case =
+                     resolve_case ~gil_case branch_kind branch_case
+                   in
+                   Ext_list.add (case, (id, Some gil_case)) ends)
+
+      let get_stack_info ~(partial : partial_data) (exec_data : exec_data) =
+        match partial.prev with
+        | None -> Ok ([], None)
+        | Some (prev_id, _, prev_callers) -> (
+            let depth_change =
+              let cs = exec_data.cmd_report.callstack in
+              assert ((List.hd cs).pid = exec_data.cmd_report.proc_name);
+              let prev_depth = List.length prev_callers in
+              List.length cs - prev_depth - 1
+            in
+            match depth_change with
+            | 0 -> Ok (prev_callers, None)
+            | 1 -> Ok (prev_id :: prev_callers, Some In)
+            | -1 -> (
+                match prev_callers with
+                | [] ->
+                    Error "HORROR - stepping out when prev_callers is empty!"
+                | hd :: tl -> Ok (tl, Some (Out hd)))
+            | _ ->
+                Error
+                  "WislLifter.compute_callers: HORROR - too great a stack \
+                   depth change!")
+
+      let update_canonical_cmd_info
+          ~id
+          ~tl_ast
+          ~annot
+          ~exec_data
+          (partial : partial_data) =
+        match (partial.display, annot.stmt_kind, annot.origin_id) with
+        | None, (Normal _ | Return _), Some origin_id ->
+            let** display =
+              get_origin_node_str tl_ast (Some origin_id)
+              |> Option.to_result ~none:"Couldn't get display!"
+            in
+            let** stack_info = get_stack_info ~partial exec_data in
+            partial.id <- Some id;
+            partial.display <- Some display;
+            partial.stack_info <- Some stack_info;
+            Ok ()
+        | _ -> Ok ()
+
+      let insert_id_and_case
+          ~prev_id
+          ~(exec_data : exec_data)
+          ~id
+          ({ all_ids; _ } : partial_data) =
+        let annot, gil_case =
+          let { cmd_report; _ } = exec_data in
+          CmdReport.(cmd_report.annot, cmd_report.branch_case)
+        in
+        let prev_kind_case =
+          let* prev_id = prev_id in
+          Ext_list.assoc_opt prev_id all_ids
+        in
+        let kind = annot.branch_kind in
+        let++ case =
+          match prev_kind_case with
+          | None -> Ok Unknown
+          | Some (prev_kind, prev_case) ->
+              resolve_case ?gil_case prev_kind prev_case
+        in
+        Ext_list.add (id, (kind, case)) all_ids;
+        (kind, case)
+
+      (** Returns whether this function would be called compositionally *)
+      let is_fcall_using_spec fn (prog : (annot, int) Prog.t) =
+        let open Gillian.Utils in
+        (match !Config.current_exec_mode with
+        | Exec_mode.Verification | Exec_mode.BiAbduction -> true
+        | Exec_mode.Concrete | Exec_mode.Symbolic -> false)
+        &&
+        match Hashtbl.find_opt prog.procs fn with
+        | Some proc -> Option.is_some proc.proc_spec
+        | None -> false
+
+      let update_submap ~prog ~(annot : Annot.t) partial =
+        match (partial.nest_kind, annot.nest_kind) with
+        | None, Some (FunCall fn) when not (is_fcall_using_spec fn prog) ->
+            partial.nest_kind <- Some (FunCall fn);
+            Ok ()
+        | None, nest ->
+            partial.nest_kind <- nest;
+            Ok ()
+        | Some _, (None | Some (FunCall _)) -> Ok ()
+        | Some _, Some _ -> Error "HORROR - multiple submaps!"
+
+      let f ~tl_ast ~prog ~prev_id ~is_loop_func ~proc_name exec_data partial =
+        let { id; cmd_report; errors; unifys; _ } = exec_data in
+        let annot = CmdReport.(cmd_report.annot) in
+        let** branch_kind, branch_case =
+          insert_id_and_case ~prev_id ~exec_data ~id partial
+        in
+        let** () = update_paths ~exec_data ~branch_case ~branch_kind partial in
+        let** () =
+          update_canonical_cmd_info ~id ~tl_ast ~annot ~exec_data partial
+        in
+        let** () = update_submap ~prog ~annot partial in
+        Ext_list.add_all errors partial.errors;
+        Ext_list.add_all unifys partial.unifys;
+
+        (* Finish or continue *)
+        match Stack.pop_opt partial.unexplored_paths with
+        | None -> finish ~is_loop_func ~proc_name ~exec_data partial
+        | Some (id, branch_case) -> step_again ~id ?branch_case ()
+    end
+
+    let update = Update.f
+
+    let find_or_init ~partials ~get_prev ~exec_data prev_id =
+      let ({ id; _ } : exec_data) = exec_data in
+      let partial =
+        let* prev_id = prev_id in
+        let () =
+          DL.log (fun m ->
+              let t_json =
+                partials |> to_yojson |> Yojson.Safe.pretty_to_string
+              in
+              m "%a: Looking for prev_id %a in:\n%s" pp_rid id pp_rid prev_id
+                t_json)
+        in
+        Hashtbl.find_opt partials prev_id
       in
-      match result with
-      | Some r -> r
-      | None -> (
-          match d.unexplored_paths |> Stack.pop_opt with
-          | Some path ->
-              let id, gil_case = List.hd path in
-              d.inner_path <- path;
-              StepAgain (Some id, gil_case)
-          | None -> make_finished_partial is_final d)
-
-    let create annot tl_ast =
-      match annot.stmt_kind with
-      | Multi NotEnd ->
-          let* origin_id = annot.origin_id in
-          let+ display = get_origin_node_str tl_ast (Some origin_id) in
-          make_partial_data display
-      | _ -> None
+      match partial with
+      | Some p -> Ok p
+      | None ->
+          let++ prev = get_prev () in
+          init_partial ~prev
 
-    let handle exec_data tl_ast partial_cmds =
-      let annot =
-        let cmd_report = exec_data.cmd_report in
-        CmdReport.(cmd_report.annot)
+    let failwith ~exec_data ?partial ~partials msg =
+      DL.failwith
+        (fun () ->
+          [
+            ("exec_data", exec_data_to_yojson exec_data);
+            ("partial_data", opt_to_yojson partial_data_to_yojson partial);
+            ("partials_state", to_yojson partials);
+          ])
+        ("WislLifter.PartialCmds.handle: " ^ msg)
+
+    let handle
+        ~(partials : t)
+        ~tl_ast
+        ~prog
+        ~get_prev
+        ~is_loop_func
+        ~proc_name
+        ~prev_id
+        exec_data =
+      let partial =
+        find_or_init ~partials ~get_prev ~exec_data prev_id
+        |> Result_utils.or_else (fun e -> failwith ~exec_data ~partials e)
       in
-      let* origin_id = annot.origin_id in
-      let+ partial_data =
-        match Hashtbl.find_opt partial_cmds origin_id with
-        | None ->
-            let+ pd = create annot tl_ast in
-            Hashtbl.add partial_cmds origin_id pd;
-            pd
-        | pd -> pd
+      Hashtbl.replace partials exec_data.id partial;
+      let result =
+        update ~tl_ast ~prog ~prev_id ~is_loop_func ~proc_name exec_data partial
+        |> Result_utils.or_else (fun e ->
+               failwith ~exec_data ~partial ~partials e)
+      in
+      let () =
+        match result with
+        | Finished _ ->
+            partial.all_ids
+            |> Ext_list.iter (fun (id, _) -> Hashtbl.remove_all partials id)
+        | _ -> ()
       in
-      let result = update annot partial_data exec_data in
-      (match result with
-      | Finished _ -> Hashtbl.remove partial_cmds origin_id
-      | _ -> ());
       result
   end
 
@@ -266,10 +473,10 @@ struct
     proc_name : string;
     gil_state : Gil_lifter.t; [@to_yojson Gil_lifter.dump]
     tl_ast : tl_ast; [@to_yojson fun _ -> `Null]
-    partial_cmds : PartialCmds.t;
+    partial_cmds : Partial_cmds.t;
     mutable map : map;
     id_map : (rid, map) Hashtbl.t; [@to_yojson fun _ -> `Null]
-    mutable before_partial : (rid * BranchCase.t option) option;
+    mutable before_partial : (rid * Gil_branch_case.t option) option;
     mutable is_loop_func : bool;
     prog : (annot, int) Prog.t; [@to_yojson fun _ -> `Null]
     func_return_data : (rid, string * int ref) Hashtbl.t;
@@ -277,39 +484,9 @@ struct
   }
   [@@deriving to_yojson]
 
-  let path_of_map = function
-    | Nothing -> []
-    | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } ->
-        data.branch_path
-
-  let gil_path_of_map = function
-    | Nothing -> []
-    | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } ->
-        data.gil_branch_path
-
-  let id_of_map ?(last = false) = function
-    | Nothing -> None
-    | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } ->
-        if last then Some (List.hd (List.rev data.ids))
-        else Some (List.hd data.ids)
-
-  let id_of_map_exn ?(last = false) map =
-    match id_of_map ~last map with
-    | None -> failwith "id_of_map: Nothing"
-    | Some id -> id
-
-  let cmd_data_of_map = function
-    | Nothing -> None
-    | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> Some data
-
-  let cmd_data_of_map_exn map =
-    match cmd_data_of_map map with
-    | None -> failwith "cmd_data_of_map: Nothing"
-    | Some callers -> callers
-
   let dump = to_yojson
 
-  module Init_or_handle = struct
+  module Insert_new_cmd = struct
     let new_function_return_label caller_id state =
       state.func_return_count <- state.func_return_count + 1;
       let label = int_to_letters state.func_return_count in
@@ -317,265 +494,161 @@ struct
       Hashtbl.add state.func_return_data caller_id (label, count);
       (label, count)
 
-    let update_caller_branches ~caller_id ~cont_id func_return_label state =
+    let update_caller_branches ~caller_id ~cont_id (label, ix) state =
       match Hashtbl.find_opt state.id_map caller_id with
       | None ->
-          Fmt.failwith "update_caller_branches: caller %a not found" pp_rid
+          Fmt.error "update_caller_branches - caller %a not found" pp_rid
             caller_id
       | Some (BranchCmd { nexts; _ }) ->
           Hashtbl.remove nexts FuncExitPlaceholder;
-          let case = FuncExit func_return_label in
+          let case = Case (FuncExit label, ix) in
           let bdata = (cont_id, None) in
-          Hashtbl.add nexts case (bdata, Nothing)
+          Hashtbl.add nexts case (bdata, Nothing);
+          Ok ()
       | Some _ ->
-          Fmt.failwith "update_caller_branches: caller %a does not branch"
-            pp_rid caller_id
+          Fmt.error "update_caller_branches - caller %a does not branch" pp_rid
+            caller_id
 
-    let new_cmd
-        state
-        kind
-        ids
-        display
-        unifys
-        errors
-        gil_branch_path
-        ?(submap = NoSubmap)
-        ~parent
-        ~callers
-        () : map =
-      let branch_path =
-        match parent with
-        | None -> []
-        | Some (parent_map, case) -> (
-            let parent_path = path_of_map parent_map in
-            match case with
-            | None -> parent_path
-            | Some (_, case) -> case :: parent_path)
-      in
-      let func_return_label =
-        match (kind, callers) with
-        | Final, caller_id :: _ ->
-            let label, count =
-              match Hashtbl.find_opt state.func_return_data caller_id with
-              | Some (label, count) -> (label, count)
-              | None -> new_function_return_label caller_id state
-            in
-            incr count;
-            let label = (label, !count) in
-            let cont_id = ids |> List.rev |> List.hd in
-            update_caller_branches ~caller_id ~cont_id label state;
-            Some label
-        | _ -> None
+    let resolve_func_branches ~state finished_partial =
+      let Partial_cmds.{ all_ids; kind; callers; _ } = finished_partial in
+      match (kind, callers) with
+      | Final, caller_id :: _ ->
+          let label, count =
+            match Hashtbl.find_opt state.func_return_data caller_id with
+            | Some (label, count) -> (label, count)
+            | None -> new_function_return_label caller_id state
+          in
+          incr count;
+          let label = (label, !count) in
+          let cont_id = all_ids |> List.rev |> List.hd in
+          let** () = update_caller_branches ~caller_id ~cont_id label state in
+          Ok (Some label)
+      | _ -> Ok None
+
+    let make_new_cmd ~func_return_label finished_partial : map =
+      let Partial_cmds.
+            {
+              all_ids;
+              id;
+              display;
+              unifys;
+              errors;
+              submap;
+              prev;
+              callers;
+              kind;
+              _;
+            } =
+        finished_partial
       in
       let data =
         {
-          ids;
+          all_ids;
+          id;
           display;
           unifys;
           errors;
           submap;
-          gil_branch_path;
-          branch_path;
-          parent;
+          prev;
           callers;
           func_return_label;
         }
       in
-      let cmd =
-        match kind with
-        | Normal -> Cmd { data; next = Nothing }
-        | Branch cases -> (
-            match cases with
-            | [ (Gil _, (_, None)) ] -> Cmd { data; next = Nothing }
-            | _ ->
-                let nexts = Hashtbl.create (List.length cases) in
-                cases
-                |> List.iter (fun (case, bdata) ->
-                       Hashtbl.add nexts case (bdata, Nothing));
-                BranchCmd { data; nexts })
-        | Final -> FinalCmd { data }
+      match kind with
+      | Final -> FinalCmd { data }
+      | Normal -> Cmd { data; next = Nothing }
+      | Branch ends ->
+          let nexts = Hashtbl.create 0 in
+          List.iter
+            (fun (case, branch_data) ->
+              Hashtbl.add nexts case (branch_data, Nothing))
+            ends;
+          BranchCmd { data; nexts }
+
+    let insert_as_next ~state ~prev_id ?case new_cmd =
+      match (Hashtbl.find state.id_map prev_id, case) with
+      | Nothing, _ -> Error "trying to insert next of Nothing!"
+      | FinalCmd _, _ -> Error "trying to insert next of FinalCmd!"
+      | Cmd _, Some _ -> Error "tying to insert to non-branch cmd with branch!"
+      | BranchCmd _, None ->
+          Error "trying to insert to branch cmd with no branch!"
+      | Cmd c, None ->
+          c.next <- new_cmd;
+          Ok ()
+      | BranchCmd { nexts; _ }, Some case -> (
+          match Hashtbl.find nexts case with
+          | branch_data, Nothing ->
+              Hashtbl.replace nexts case (branch_data, new_cmd);
+              Ok ()
+          | _ -> Error "duplicate insertion!")
+
+    let insert_as_submap ~state ~parent_id new_cmd =
+      let** parent_data =
+        match Hashtbl.find state.id_map parent_id with
+        | Nothing -> Error "trying to insert submap of Nothing!"
+        | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> Ok data
       in
-      ids |> List.iter (fun id -> Hashtbl.replace state.id_map id cmd);
-      cmd
+      match parent_data.submap with
+      | Proc _ | Submap _ -> Error "duplicate submaps!"
+      | NoSubmap ->
+          parent_data.submap <- Submap new_cmd;
+          Ok ()
+
+    let insert_cmd ~state ~prev ~stack_direction ~func_return_label new_cmd =
+      match (stack_direction, state.map, prev) with
+      | Some _, Nothing, _ -> Error "stepping in our out with empty map!"
+      | _, Nothing, Some _ -> Error "inserting to empty map with prev!"
+      | None, Nothing, None ->
+          state.map <- new_cmd;
+          Ok ()
+      | _, _, None -> Error "inserting to non-empty map with no prev!"
+      | Some In, _, Some (_, Some _) -> Error "stepping in with branch case!"
+      | Some In, _, Some (parent_id, None) ->
+          insert_as_submap ~state ~parent_id new_cmd
+      | None, _, Some (prev_id, case) ->
+          insert_as_next ~state ~prev_id ?case new_cmd
+      | Some (Out prev_id), _, _ ->
+          let** case =
+            match func_return_label with
+            | Some (label, ix) -> Ok (Case (FuncExit label, ix))
+            | None -> Error "stepping out without function return label!"
+          in
+          insert_as_next ~state ~prev_id ~case new_cmd
 
-    let convert_kind id kind =
-      let json cases =
-        let cmd_kind_to_yojson =
-          cmd_kind_to_yojson BranchCase.to_yojson (fun () -> `Null)
+    let f ~state finished_partial =
+      let r =
+        let { id_map; _ } = state in
+        let Partial_cmds.{ all_ids; prev; stack_direction; _ } =
+          finished_partial
+        in
+        let** func_return_label =
+          resolve_func_branches ~state finished_partial
         in
-        let cases_to_yojson cases =
-          cases |> List.map fst |> list_to_yojson BranchCase.to_yojson
+        let new_cmd = make_new_cmd ~func_return_label finished_partial in
+        let** () =
+          insert_cmd ~state ~prev ~stack_direction ~func_return_label new_cmd
         in
-        [
-          ("id", L.Report_id.to_yojson id);
-          ("kind", cmd_kind_to_yojson kind);
-          ("cases", cases_to_yojson cases);
-        ]
+        all_ids |> List.iter (fun id -> Hashtbl.replace id_map id new_cmd);
+        Ok ()
       in
-      let failwith cases msg = DL.failwith (fun () -> json cases) msg in
-      match kind with
-      | Normal -> Normal
-      | Final -> Final
-      | Branch cases -> (
-          match cases with
-          | (BranchCase.GuardedGoto _, ()) :: _ ->
-              let cases =
-                cases
-                |> List.map (fun (case, _) ->
-                       match case with
-                       | BranchCase.GuardedGoto b -> (IfElse b, (id, Some case))
-                       | _ ->
-                           failwith cases
-                             "convert_kind: inconsistent branch cases!")
-              in
-              Branch cases
-          | (BranchCase.LCmd _, ()) :: _ ->
-              let cases =
-                cases
-                |> List.map (fun (case, _) ->
-                       match case with
-                       | BranchCase.LCmd lcmd -> (LCmd lcmd, (id, Some case))
-                       | _ ->
-                           failwith cases
-                             "convert_kind: inconsistent branch cases!")
-              in
-              Branch cases
-          | _ ->
-              DL.log (fun m ->
-                  m ~json:(json cases)
-                    "convert_kind: WARNING - unknown branch case!");
-              let cases =
-                cases |> List.mapi (fun i (case, _) -> (Gil i, (id, Some case)))
-              in
-              Branch cases)
+      r
+      |> Result_utils.or_else (fun e ->
+             DL.failwith
+               (fun () ->
+                 [
+                   ("state", dump state);
+                   ( "finished_partial",
+                     Partial_cmds.finished_to_yojson finished_partial );
+                 ])
+               ("WislLifter.insert_new_cmd: " ^ e))
+  end
 
-    (** If the given ID isn't in the map, attempt to step backwards through the
-    GIL map until an ID (and map node) that *is* in the lifted map is found. *)
-    let rec get_prev_in_map id state =
-      match Hashtbl.find_opt state.id_map id with
-      | None -> (
-          DL.log (fun m ->
-              m "couldn't find id %a; attempting with previous step from GIL."
-                pp_rid id);
-          match state.gil_state |> Gil_lifter.previous_step id with
-          | None -> None
-          | Some (prev_id, _) -> get_prev_in_map prev_id state)
-      | Some map -> Some (id, map)
-
-    let insert_new_cmd
-        (new_cmd : parent:parent -> unit -> map)
-        (new_id : rid)
-        (id : rid)
-        (gil_case : BranchCase.t option)
-        (stack_direction : stack_direction option)
-        state =
-      let failwith s = failwith ("WislLifter.insert_new_cmd: " ^ s) in
-      let map =
-        match stack_direction with
-        | Some (Out id) -> Hashtbl.find state.id_map id
-        | _ -> (
-            match get_prev_in_map id state with
-            | None ->
-                failwith
-                  (Fmt.str "Couldn't get prev command of '%a'!" pp_rid id)
-            | Some (_, map) -> map)
-      in
-      match (stack_direction, map) with
-      (* First command in a (nested) function call *)
-      | Some In, (Cmd { data; _ } | BranchCmd { data; _ }) ->
-          assert (data.submap = NoSubmap);
-          data.submap <- Submap (new_cmd ~parent:None ())
-      | _, Cmd c ->
-          let parent = Some (map, None) in
-          c.next <- new_cmd ~parent ()
-      | _, BranchCmd { nexts; _ } ->
-          (* If applicable, find the (empty) branch that will be replaced*)
-          let case, next, bdata =
-            match gil_case with
-            | None ->
-                let rec aux new_id =
-                  let result =
-                    nexts
-                    |> Hashtbl.find_map (fun case (bdata, next) ->
-                           match bdata with
-                           | case_id, _ when case_id = new_id ->
-                               Some (case, next, bdata)
-                           | _ -> None)
-                  in
-                  match result with
-                  | Some r -> r
-                  | None -> (
-                      let prev =
-                        state.gil_state |> Gil_lifter.previous_step new_id
-                      in
-                      match prev with
-                      | Some (new_id, _) ->
-                          DL.log (fun m ->
-                              m
-                                "Inserting without gil case; attempting to \
-                                 look back for link (prev: %a)"
-                                L.Report_id.pp new_id);
-                          aux new_id
-                      | _ ->
-                          failwith
-                            "HORROR - tried to insert without branch case!")
-                in
-                aux new_id
-            | Some gil_case ->
-                Hashtbl.find_map
-                  (fun case (bdata, next) ->
-                    let gil_case' = bdata |> snd |> Option.get in
-                    if gil_case <> gil_case' then None
-                    else Some (case, next, bdata))
-                  nexts
-                |> Option.get
-          in
-          if next <> Nothing then
-            failwith "HORROR - tried to insert to non-Nothing!";
-          let parent = Some (map, Some (bdata, case)) in
-          Hashtbl.replace nexts case (bdata, new_cmd ~parent ())
-      | _ -> failwith "HORROR - tried to insert to FinalCmd or Nothing!"
-
-    let is_fcall_using_spec fn (prog : (annot, int) Prog.t) =
-      let open Gillian.Utils in
-      (match !Config.current_exec_mode with
-      | Exec_mode.Verification | Exec_mode.BiAbduction -> true
-      | Exec_mode.Concrete | Exec_mode.Symbolic -> false)
-      &&
-      match Hashtbl.find_opt prog.procs fn with
-      | Some proc -> Option.is_some proc.proc_spec
-      | None -> false
-
-    let prepare_basic_cmd ?display ?(final = false) tl_ast id_map prog exec_data
-        =
-      let { cmd_report; _ } = exec_data in
-      let annot = CmdReport.(cmd_report.annot) in
-      let { origin_id; nest_kind; _ } = annot in
-      let display =
-        match display with
-        | Some d -> d
-        | None ->
-            get_origin_node_str tl_ast origin_id
-            |> Option.value ~default:"Unknown command!"
-      in
-      let { id; unifys; errors; branch_path = gil_branch_path; kind; _ } =
-        exec_data
-      in
-      let submap =
-        match nest_kind with
-        | LoopBody p -> Proc p
-        | _ -> NoSubmap
-      in
-      let kind =
-        if final then Final
-        else
-          match nest_kind with
-          | FunCall fn when not (is_fcall_using_spec fn prog) ->
-              Branch [ (FuncExitPlaceholder, (id, None)) ]
-          | _ -> convert_kind id kind
-      in
-      new_cmd id_map kind [ id ] display unifys errors gil_branch_path ~submap
+  let insert_new_cmd = Insert_new_cmd.f
 
+  module Init_or_handle = struct
+    (** Loop body functions have some boilerplate we want to ignore.
+        This would normally be [Hidden], but we want to only consider
+        the true case of the function *)
     let handle_loop_prefix exec_data =
       let annot = CmdReport.(exec_data.cmd_report.annot) in
       match annot.stmt_kind with
@@ -583,150 +656,63 @@ struct
           Some
             (match exec_data.cmd_report.cmd with
             | Cmd.GuardedGoto _ ->
-                ExecNext (None, Some (BranchCase.GuardedGoto true))
+                ExecNext (None, Some (Gil_branch_case.GuardedGoto true))
             | _ -> ExecNext (None, None))
       | _ -> None
 
-    let compute_callers prev_id (exec_data : exec_data) state :
-        rid list * stack_direction option =
-      let prev =
-        let* prev_id = prev_id in
-        get_prev_in_map prev_id state
+    let get_prev ~state ~gil_case ~prev_id () =
+      let { map; id_map; _ } = state in
+      let=* prev_id = Ok prev_id in
+      let=* map =
+        match Hashtbl.find_opt id_map prev_id with
+        | None -> (
+            match map with
+            | Nothing -> Ok None
+            | _ -> Error "couldn't find map at prev_id!")
+        | map -> Ok map
       in
-      match prev with
-      | None -> ([], None)
-      | Some (prev_id, prev_node) -> (
-          let prev = cmd_data_of_map_exn prev_node in
-          let depth_change =
-            let cs = exec_data.cmd_report.callstack in
-            assert ((List.hd cs).pid = exec_data.cmd_report.proc_name);
-            let prev_depth = List.length prev.callers in
-            List.length cs - prev_depth - 1
+      match map with
+      | Nothing -> Error "got Nothing map!"
+      | FinalCmd _ -> Error "prev map is Final!"
+      | Cmd { data; _ } -> Ok (Some (data.id, None, data.callers))
+      | BranchCmd { data; nexts } -> (
+          let case =
+            Hashtbl.find_map
+              (fun case ((id, gil_case'), _) ->
+                if id = prev_id && gil_case' = gil_case then Some case else None)
+              nexts
           in
-          match depth_change with
-          | 0 -> (prev.callers, None)
-          | 1 -> (prev_id :: prev.callers, Some In)
-          | -1 -> (
-              match prev.callers with
-              | [] -> failwith "HORROR - prev.callers is empty!"
-              | hd :: tl -> (tl, Some (Out hd)))
-          | _ ->
-              Fmt.failwith
-                "WislLifter.compute_callers: HORROR - cmd %a has too great a \
-                 depth change!"
-                pp_rid prev_id)
-
-    let handle_no_partial
-        callers
-        stack_direction
-        prev_id
-        branch_case
-        exec_data
-        state =
-      let Debugger.Lifter.{ id; _ } = exec_data in
-      let { tl_ast; proc_name; is_loop_func; _ } = state in
-      let display, final =
-        if is_loop_func && get_fun_call_name exec_data = Some proc_name then
-          (Some "<end of loop>", true)
-        else (None, false)
-      in
-      let new_cmd =
-        prepare_basic_cmd ?display ~final ~callers tl_ast state state.prog
-          exec_data
-      in
-      (match (state.map, prev_id) with
-      | Nothing, _ -> state.map <- new_cmd ~parent:None ()
-      | _, Some prev_id ->
-          insert_new_cmd new_cmd id prev_id branch_case stack_direction state
-      | _, _ ->
-          failwith
-            "HORROR - tried to insert to non-Nothing map without previous id!");
-      Stop
-
-    let handle_finished_partial
-        finished_data
-        callers
-        stack_direction
-        prev_id
-        branch_case
-        exec_data
-        state =
-      let Debugger.Lifter.{ id; _ } = exec_data in
-      let PartialCmds.{ ids; display; unifys; errors; cmd_kind; submap } =
-        finished_data
-      in
-      let gil_branch_path =
-        Gil_lifter.path_of_id (List.hd ids) state.gil_state
-      in
-      let new_cmd =
-        new_cmd state cmd_kind ids display unifys errors gil_branch_path ~submap
+          match case with
+          | Some case -> Ok (Some (data.id, Some case, data.callers))
+          | None -> Error "couldn't find prev in branches!")
+
+    let f ~state ?prev_id ?gil_case (exec_data : exec_data) : handle_cmd_result
+        =
+      let- () = handle_loop_prefix exec_data in
+      let gil_case =
+        Option_utils.coalesce gil_case exec_data.cmd_report.branch_case
       in
-      let prev_id, branch_case =
-        match state.before_partial with
-        | Some (prev_id, branch_case) ->
-            state.before_partial <- None;
-            (Some prev_id, branch_case)
-        | None -> (prev_id, branch_case)
+      let { tl_ast; partial_cmds = partials; is_loop_func; proc_name; prog; _ }
+          =
+        state
       in
-      (match (state.map, prev_id) with
-      (* First insertion to empty map *)
-      | Nothing, _ -> state.map <- new_cmd ~callers:[] ~parent:None ()
-      (* Normal insertion *)
-      | _, Some prev_id ->
-          insert_new_cmd (new_cmd ~callers) id prev_id branch_case
-            stack_direction state
-      | _, _ ->
-          failwith
-            "HORROR - tried to insert to non-Nothing map without previous id!");
-      Stop
-
-    let do_handle prev_id branch_case exec_data state =
-      let { tl_ast; partial_cmds; _ } = state in
-      match handle_loop_prefix exec_data with
-      | Some result ->
-          state.is_loop_func <- true;
-          result
-      | None -> (
-          let callers, stack_direction =
-            compute_callers prev_id exec_data state
-          in
-          match PartialCmds.handle exec_data tl_ast partial_cmds with
-          | Some (StepAgain result) ->
-              if Option.is_none state.before_partial then
-                prev_id
-                |> Option.iter (fun prev_id ->
-                       state.before_partial <- Some (prev_id, branch_case));
-              ExecNext result
-          | None ->
-              handle_no_partial callers stack_direction prev_id branch_case
-                exec_data state
-          | Some (Finished finished_data) ->
-              handle_finished_partial finished_data callers stack_direction
-                prev_id branch_case exec_data state)
-
-    let check_gil_to_exec result state =
-      match result with
-      | Stop -> (
-          match Gil_lifter.pop_to_exec state.gil_state with
-          | Some (id, case) -> ExecNext (Some id, case)
-          | None -> Stop)
-      | _ -> result
-
-    let f prev_id branch_case exec_data state =
-      let Debugger.Lifter.{ id; _ } = exec_data in
-      DL.log (fun m ->
-          m
-            ~json:
-              [
-                ("state", dump state);
-                ("exec_data", exec_data_to_yojson exec_data);
-                ("prev_id", (opt_to_yojson L.Report_id.to_yojson) prev_id);
-                ("branch_case", (opt_to_yojson BranchCase.to_yojson) branch_case);
-              ]
-            "HANDLING %a (prev %a)" L.Report_id.pp id (pp_option L.Report_id.pp)
-            prev_id);
-      let result = do_handle prev_id branch_case exec_data state in
-      check_gil_to_exec result state
+      match
+        let get_prev = get_prev ~state ~gil_case ~prev_id in
+        Partial_cmds.handle ~partials ~tl_ast ~prog ~get_prev ~is_loop_func
+          ~proc_name ~prev_id exec_data
+      with
+      | Finished finished ->
+          DL.log (fun m ->
+              m
+                ~json:
+                  [
+                    ("state", to_yojson state);
+                    ("finished", Partial_cmds.finished_to_yojson finished);
+                  ]
+                "Finishing WISL command");
+          insert_new_cmd ~state finished;
+          Stop (Some finished.id)
+      | StepAgain (id, case) -> ExecNext (id, case)
   end
 
   let init_or_handle = Init_or_handle.f
@@ -752,7 +738,7 @@ struct
         func_return_count = 0;
       }
     in
-    let result = init_or_handle None None exec_data state in
+    let result = init_or_handle ~state exec_data in
     (state, result)
 
   let init_exn ~proc_name ~all_procs tl_ast prog exec_data =
@@ -760,54 +746,36 @@ struct
     | None -> failwith "init: wislLifter needs a tl_ast!"
     | Some x -> x
 
-  let handle_cmd prev_id branch_case (exec_data : exec_data) state =
-    init_or_handle (Some prev_id) branch_case exec_data state
+  let handle_cmd prev_id gil_case (exec_data : exec_data) state =
+    init_or_handle ~state ~prev_id ?gil_case exec_data
 
   let get_gil_map _ = failwith "get_gil_map: not implemented!"
 
-  let package_case (bd : branch_data) (case : branch_case) all_cases :
-      Packaged.branch_case =
-    let json = branch_case_to_yojson case in
-    let kind, display =
-      match case with
-      | IfElse b -> ("IfElse", ("If/Else", Fmt.str "%B" b))
-      | LCmd x -> ("LCmd", ("Logical command", Fmt.str "%d" x))
-      | Gil x -> (
-          let id, gil_case = bd in
-          match gil_case with
-          | Some gil_case ->
-              let kind_display, _ =
-                Packaged.(package_gil_case gil_case).display
-              in
-              let kind = "GIL" in
-              let kind_display = Fmt.str "(GIL) %s" kind_display in
-              (* let display = Fmt.str "(%a) %s" pp_rid id display in *)
-              let display = Int.to_string x in
-              (kind, (kind_display, display))
-          | None -> ("GIL", ("(GIL) Unknown", Fmt.str "(%a) Unknown" pp_rid id))
-          )
-      | FuncExit (label, i) ->
-          ("FuncExit", ("Return case", Fmt.str "%s-%d" label i))
-      | FuncExitPlaceholder ->
-          ("FuncExitPlaceholder", ("Return case", "<step in>"))
-    in
-    let display =
-      match (WBranchCase.is_hidden_when_single case, all_cases) with
-      | true, [ _ ] -> ("", "")
-      | _ -> display
-    in
-    { kind; display; json }
+  let package_case case =
+    let json = Branch_case.to_yojson case in
+    let display = Branch_case.display case in
+    (display, json)
 
-  let package_data package { ids; display; unifys; errors; submap; _ } =
+  let package_data package { id; all_ids; display; unifys; errors; submap; _ } =
     let submap =
       match submap with
       | NoSubmap -> NoSubmap
       | Proc p -> Proc p
       | Submap map -> Submap (package map)
     in
-    Packaged.{ ids; display; unifys; errors; submap }
+    Packaged.{ id; all_ids; display; unifys; errors; submap }
+
+  let package =
+    let package_case
+        ~(bd : branch_data)
+        ~(all_cases : (Branch_case.t * branch_data) list)
+        case =
+      ignore bd;
+      ignore all_cases;
+      package_case case
+    in
+    Packaged.package package_data package_case
 
-  let package = Packaged.package package_data package_case
   let get_lifted_map_exn { map; _ } = package map
   let get_lifted_map state = Some (get_lifted_map_exn state)
 
@@ -821,11 +789,9 @@ struct
     match map with
     | Nothing -> None
     | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } ->
-        Some (List.hd data.ids)
+        Some data.id
 
-  let path_of_id id { id_map; _ } =
-    let map = Hashtbl.find id_map id in
-    gil_path_of_map map
+  let path_of_id id { gil_state; _ } = Gil_lifter.path_of_id id gil_state
 
   let existing_next_steps id { gil_state; id_map; _ } =
     Gil_lifter.existing_next_steps id gil_state
@@ -848,26 +814,22 @@ struct
     | Cmd _, Some _ -> failwith "got branch case at non-branch cmd!"
     | BranchCmd _, None -> failwith "expected branch case at branch cmd!"
     | Cmd { data; _ }, None ->
-        let id = List.hd (List.rev data.ids) in
+        let id = List.hd (List.rev data.all_ids) in
         (id, None)
     | BranchCmd { nexts; _ }, Some case -> (
-        let case =
-          Packaged.(case.json) |> branch_case_of_yojson |> Result.get_ok
-        in
+        let case = case |> snd |> Branch_case.of_yojson |> Result.get_ok in
         match Hashtbl.find_opt nexts case with
         | None -> failwith "branch case not found!"
         | Some ((id, case), _) -> (id, case))
 
   let previous_step id { id_map; _ } =
-    match Hashtbl.find id_map id with
-    | Nothing -> None
-    | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } ->
-        let+ parent, case = data.parent in
-        let id = id_of_map_exn parent in
-        let case =
-          case |> Option.map (fun (bdata, case) -> package_case bdata case [])
-        in
-        (id, case)
+    let+ id, case =
+      match Hashtbl.find id_map id with
+      | Nothing -> None
+      | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> data.prev
+    in
+    let case = case |> Option.map package_case in
+    (id, case)
 
   let select_next_path case id { gil_state; _ } =
     Gil_lifter.select_next_path case id gil_state
@@ -887,8 +849,8 @@ struct
                 ("at_id", opt_to_yojson rid_to_yojson at_id);
               ])
             "find_unfinished_path: started at Nothing"
-      | Cmd { data = { ids; _ }; next = Nothing } ->
-          let id = List.hd (List.rev ids) in
+      | Cmd { data = { all_ids; _ }; next = Nothing } ->
+          let id = List.hd (List.rev all_ids) in
           Some (id, None)
       | Cmd { next; _ } -> aux next
       | BranchCmd { nexts; _ } -> (
@@ -924,7 +886,6 @@ struct
     annot_to_wisl_stmt annot wisl_ast
 
   let get_cell_var_from_cmd gil_cmd wisl_ast =
-    let open Syntaxes.Option in
     match wisl_ast with
     | Some ast -> (
         let* stmt = get_wisl_stmt gil_cmd ast in
@@ -939,7 +900,6 @@ struct
         | _ -> None)
 
   let free_error_to_string msg_prefix prev_annot gil_cmd wisl_ast =
-    let open Syntaxes.Option in
     let var =
       match wisl_ast with
       | Some ast -> (
diff --git a/wisl/lib/utils/wBranchCase.ml b/wisl/lib/utils/wBranchCase.ml
index fe9224096..013d514e8 100644
--- a/wisl/lib/utils/wBranchCase.ml
+++ b/wisl/lib/utils/wBranchCase.ml
@@ -1,11 +1,29 @@
-type t =
-  | IfElse of bool
-  | LCmd of int
-  | Gil of int
-  | FuncExitPlaceholder
-  | FuncExit of (string * int)
-[@@deriving yojson]
+type kind = IfElseKind [@@deriving yojson]
+type case = IfElse of bool | FuncExit of string | Unknown [@@deriving yojson]
+type t = Case of case * int | FuncExitPlaceholder [@@deriving yojson]
 
-let is_hidden_when_single = function
-  | Gil _ | FuncExit _ -> true
-  | _ -> false
+let display = function
+  | Case (Unknown, i) -> Fmt.str "%d" i
+  | Case (IfElse b, -1) -> Fmt.str "%B" b
+  | Case (IfElse b, i) -> Fmt.str "%B - %d" b i
+  | Case (FuncExit label, i) -> Fmt.str "%s-%d" label i
+  | FuncExitPlaceholder -> "<step in>"
+
+let compare a b =
+  let compare_pair (a1, a2) (b1, b2) =
+    let cmp = Int.compare a1 b1 in
+    if cmp = 0 then String.compare a2 b2 else cmp
+  in
+  let get_ix = function
+    | FuncExitPlaceholder -> (0, "")
+    | Case (IfElse false, _) -> (1, "")
+    | Case (IfElse true, _) -> (2, "")
+    | Case (FuncExit l, _) -> (3, l)
+    | Case (Unknown, _) -> (4, "")
+  in
+  let cmp = compare_pair (get_ix a) (get_ix b) in
+  match (cmp, a, b) with
+  | 0, FuncExitPlaceholder, _ | 0, _, FuncExitPlaceholder ->
+      failwith "impossible"
+  | 0, Case (_, a), Case (_, b) -> Int.compare a b
+  | cmp, _, _ -> cmp