diff --git a/CHANGES.md b/CHANGES.md
index 1b8685048..3cbb9677f 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,6 @@
 ## unreleased
 
+- parameterize the `Thread` module on the symbolic memory and the `Choice_monad` module on a Thread
 - adds a `owi_char` function to create char symbolic value
 - adds a `Mem` argument to external function to allow direct manipulation of the memory.
 - support other solvers through the `--solver` option (Z3, Colibri2, Bitwuzla and CVC5)
diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml
index ad120ab6f..f61287521 100644
--- a/src/cmd/cmd_sym.ml
+++ b/src/cmd/cmd_sym.ml
@@ -4,7 +4,7 @@
 
 open Syntax
 module Expr = Smtml.Expr
-module Choice = Symbolic.P.Choice
+module Choice = Symbolic_choice_with_memory
 
 let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) :
   'b Result.t Choice.t =
@@ -46,14 +46,15 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   let* _created_dir = Bos.OS.Dir.create ~path:true ~mode:0o755 workspace in
   let pc = Choice.return (Ok ()) in
   let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
-  let thread : Thread.t = Thread.create () in
+  let thread = Thread_with_memory.init () in
   let res_queue = Wq.init () in
-  let callback = function
-    | Symbolic_choice.EVal (Ok ()), _ -> ()
+  let callback v =
+    match v with
+    | Symbolic_choice_intf.EVal (Ok ()), _ -> ()
     | v -> Wq.push v res_queue
   in
   let join_handles =
-    Symbolic_choice.run ~workers solver result thread ~callback
+    Symbolic_choice_with_memory.run ~workers solver result thread ~callback
       ~callback_init:(fun () -> Wq.make_pledge res_queue)
       ~callback_end:(fun () -> Wq.end_pledge res_queue)
   in
@@ -74,7 +75,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
     | Seq.Nil -> Ok count_acc
     | Seq.Cons ((result, _thread), tl) ->
       let* model =
-        let open Symbolic_choice in
+        let open Symbolic_choice_intf in
         match result with
         | EAssert (assertion, model) ->
           print_bug (`EAssert (assertion, model));
@@ -100,7 +101,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
     if deterministic_result_order then
       results
       |> Seq.map (function (_, thread) as x ->
-           (x, List.rev @@ Thread.breadcrumbs thread) )
+           (x, List.rev @@ Thread_with_memory.breadcrumbs thread) )
       |> List.of_seq
       |> List.sort (fun (_, bc1) (_, bc2) ->
              List.compare Prelude.Int32.compare bc1 bc2 )
diff --git a/src/dune b/src/dune
index 4fa1fca25..d95dc021c 100644
--- a/src/dune
+++ b/src/dune
@@ -61,7 +61,10 @@
   solver
   symbolic
   symbolic_choice
+  symbolic_choice_intf
   symbolic_choice_minimalist
+  symbolic_choice_with_memory
+  symbolic_choice_without_memory
   symbolic_global
   symbolic_memory
   symbolic_table
@@ -75,6 +78,9 @@
   text_lexer
   text_parser
   thread
+  thread_intf
+  thread_with_memory
+  thread_without_memory
   tracing
   trap
   typecheck
diff --git a/src/intf/choice_intf.ml b/src/intf/choice_intf.ml
index ef40a4742..ad69f8336 100644
--- a/src/intf/choice_intf.ml
+++ b/src/intf/choice_intf.ml
@@ -40,4 +40,6 @@ module type Complete = sig
   val thread : thread t
 
   val add_pc : V.vbool -> unit t
+
+  val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
 end
diff --git a/src/intf/symbolic_choice_intf.ml b/src/intf/symbolic_choice_intf.ml
new file mode 100644
index 000000000..1c39b7ab0
--- /dev/null
+++ b/src/intf/symbolic_choice_intf.ml
@@ -0,0 +1,81 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+type 'a eval =
+  | EVal of 'a
+  | ETrap of Trap.t * Smtml.Model.t
+  | EAssert of Smtml.Expr.t * Smtml.Model.t
+
+module type S = sig
+  module V : Func_intf.Value_types
+
+  type thread
+
+  type 'a t
+
+  val return : 'a -> 'a t
+
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
+
+  val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+  val map : 'a t -> ('a -> 'b) -> 'b t
+
+  val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+  val trap : Trap.t -> 'a t
+
+  val select : V.vbool -> bool t
+
+  val select_i32 : V.int32 -> Int32.t t
+
+  val assertion : V.vbool -> unit t
+
+  val with_thread : (thread -> 'a) -> 'a t
+
+  val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
+
+  val solver : Solver.t t
+
+  val thread : thread t
+
+  val add_pc : V.vbool -> unit t
+
+  type 'a run_result = ('a eval * thread) Seq.t
+
+  val run :
+       workers:int
+    -> Smtml.Solver_dispatcher.solver_type
+    -> 'a t
+    -> thread
+    -> callback:('a eval * thread -> unit)
+    -> callback_init:(unit -> unit)
+    -> callback_end:(unit -> unit)
+    -> unit Domain.t array
+end
+
+module type Intf = sig
+  module type S = S
+
+  module CoreImpl : sig
+    (* The core implementation of the monad. It is isolated in a module to *)
+    (* restict its exposed interface and maintain its invariant. *)
+
+    module State : sig
+      type ('a, 's) t
+
+      val project_state :
+           ('st1 -> 'st2 * 'backup)
+        -> ('backup -> 'st2 -> 'st1)
+        -> ('a, 'st2) t
+        -> ('a, 'st1) t
+    end
+  end
+
+  module Make (Thread : Thread.S) :
+    S
+      with type 'a t = ('a eval, Thread.t) CoreImpl.State.t
+       and type thread := Thread.t
+       and module V := Symbolic_value
+end
diff --git a/src/intf/thread_intf.ml b/src/intf/thread_intf.ml
new file mode 100644
index 000000000..476de531f
--- /dev/null
+++ b/src/intf/thread_intf.ml
@@ -0,0 +1,62 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+module type M = sig
+  type collection
+
+  val init : unit -> collection
+
+  val clone : collection -> collection
+end
+
+module type S = sig
+  type t
+
+  module Memory : M
+
+  val init : unit -> t
+
+  val create :
+       int
+    -> Smtml.Symbol.t list
+    -> Symbolic_value.vbool list
+    -> Memory.collection
+    -> Symbolic_table.collection
+    -> Symbolic_global.collection
+    -> int32 list
+    -> t
+
+  val pc : t -> Symbolic_value.vbool list
+
+  val memories : t -> Memory.collection
+
+  val tables : t -> Symbolic_table.collection
+
+  val globals : t -> Symbolic_global.collection
+
+  val breadcrumbs : t -> int32 list
+
+  val symbols_set : t -> Smtml.Symbol.t list
+
+  val symbols : t -> int
+
+  val clone : t -> t
+
+  val add_pc : t -> Symbolic_value.vbool -> t
+
+  val add_breadcrumb : t -> int32 -> t
+
+  val add_symbol : t -> Smtml.Symbol.t -> t
+
+  val incr_symbols : t -> t
+end
+
+module type Intf = sig
+  module type M = M
+
+  module type S = S
+
+  module Make (Symbolic_memory : M) :
+    S with type Memory.collection = Symbolic_memory.collection
+end
diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml
index 8b64f67e9..c33009e98 100644
--- a/src/symbolic/symbolic.ml
+++ b/src/symbolic/symbolic.ml
@@ -2,20 +2,8 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-module type Thread = sig
-  type t
-
-  val memories : t -> Symbolic_memory.collection
-
-  val tables : t -> Symbolic_table.collection
-
-  val globals : t -> Symbolic_global.collection
-
-  val pc : t -> Symbolic_value.vbool list
-end
-
 module MakeP
-    (Thread : Thread)
+    (Thread : Thread.S with type Memory.collection = Symbolic_memory.collection)
     (Choice : Choice_intf.Complete
                 with module V := Symbolic_value
                  and type thread := Thread.t) =
@@ -180,8 +168,10 @@ struct
   end
 end
 
-module P = MakeP [@inlined hint] (Thread) (Symbolic_choice)
-module M = MakeP [@inlined hint] (Thread) (Symbolic_choice_minimalist)
+module P =
+  MakeP [@inlined hint] (Thread_with_memory) (Symbolic_choice_with_memory)
+module M =
+  MakeP [@inlined hint] (Thread_with_memory) (Symbolic_choice_minimalist)
 
 let convert_module_to_run (m : 'f Link.module_to_run) =
   P.Module_to_run.{ modul = m.modul; env = m.env; to_run = m.to_run }
diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml
index 05de59027..322d883c0 100644
--- a/src/symbolic/symbolic_choice.ml
+++ b/src/symbolic/symbolic_choice.ml
@@ -2,6 +2,8 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
+include Symbolic_choice_intf
+
 (*
      Multicore is based on several layers of monad transformers defined here
      in submodules. The module as a whole is made to provide a monad to explore in parallel
@@ -16,65 +18,7 @@ module Prio = struct
   let default = Default
 end
 
-module CoreImpl : sig
-  (*
-      The core implementation of the monad. It is isolated in a module to restict its exposed interface
-      and maintain its invariant. In particular, choose must guarantee that the Thread.t is cloned in each branch.
-      Using functions defined here should be foolproof.
-    *)
-  type 'a t
-
-  val return : 'a -> 'a t
-
-  val bind : 'a t -> ('a -> 'b t) -> 'b t
-
-  val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
-
-  val map : 'a t -> ('a -> 'b) -> 'b t
-
-  val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
-
-  val stop : 'a t
-
-  val assertion_fail : Smtml.Expr.t -> Smtml.Model.t -> 'a t
-
-  val trap : Trap.t -> 'a t
-
-  val thread : Thread.t t
-
-  val yield : unit t
-
-  val solver : Solver.t t
-
-  val with_thread : (Thread.t -> 'a) -> 'a t
-
-  val set_thread : Thread.t -> unit t
-
-  val modify_thread : (Thread.t -> Thread.t) -> unit t
-
-  (*
-       Indicates a possible choice between two values. Thread duplication
-       is already handled by choose and should not be done before by the caller.
-    *)
-  val choose : 'a t -> 'a t -> 'a t
-
-  type 'a eval =
-    | EVal of 'a
-    | ETrap of Trap.t * Smtml.Model.t
-    | EAssert of Smtml.Expr.t * Smtml.Model.t
-
-  type 'a run_result = ('a eval * Thread.t) Seq.t
-
-  val run :
-       workers:int
-    -> Smtml.Solver_dispatcher.solver_type
-    -> 'a t
-    -> Thread.t
-    -> callback:('a eval * Thread.t -> unit)
-    -> callback_init:(unit -> unit)
-    -> callback_end:(unit -> unit)
-    -> unit Domain.t array
-end = struct
+module CoreImpl = struct
   module Schedulable = struct
     (*
         A monad representing computation that can be cooperatively scheduled and may need
@@ -182,16 +126,16 @@ end = struct
       *)
     module M = Schedulable
 
-    type 'a t = St of (Thread.t -> ('a * Thread.t, Solver.t) M.t) [@@unboxed]
+    type ('a, 's) t = St of ('s -> ('a * 's, Solver.t) M.t) [@@unboxed]
 
     let run (St mxf) st = mxf st
 
     let return x = St (fun st -> M.return (x, st))
 
-    let lift x =
+    let lift (x : ('a, _) M.t) : ('a, 's) t =
       let ( let+ ) = M.( let+ ) in
       St
-        (fun st ->
+        (fun (st : 's) ->
           let+ x in
           (x, st) )
 
@@ -215,6 +159,15 @@ end = struct
     let with_state f = St (fun st -> M.return (f st))
 
     let modify_state f = St (fun st -> M.return ((), f st))
+
+    let project_state (project_and_backup : 'st1 -> 'st2 * 'backup) restore
+      other =
+      St
+        (fun st ->
+          let ( let+ ) = M.( let+ ) in
+          let proj, backup = project_and_backup st in
+          let+ res, new_state = run other proj in
+          (res, restore backup new_state) )
   end
 
   module Eval = struct
@@ -224,12 +177,7 @@ end = struct
       *)
     module M = State
 
-    type 'a eval =
-      | EVal of 'a
-      | ETrap of Trap.t * Smtml.Model.t
-      | EAssert of Smtml.Expr.t * Smtml.Model.t
-
-    type 'a t = 'a eval M.t
+    type ('a, 's) t = ('a eval, 's) M.t
 
     let return x : _ t = M.return (EVal x)
 
@@ -259,210 +207,276 @@ end = struct
     let ( let+ ) = map
   end
 
-  include Eval
+  module Make (Thread : Thread.S) : sig
+    (*
+      The core implementation of the monad. It is isolated in a module to restict its exposed interface
+      and maintain its invariant. In particular, choose must guarantee that the Thread.t is cloned in each branch.
+      Using functions defined here should be foolproof.
+    *)
 
-  (*
+    type thread := Thread.t
+
+    type 'a t = ('a, Thread.t) Eval.t
+
+    val return : 'a -> 'a t
+
+    val bind : 'a t -> ('a -> 'b t) -> 'b t
+
+    val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+    val map : 'a t -> ('a -> 'b) -> 'b t
+
+    val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+    val assertion_fail : Smtml.Expr.t -> Smtml.Model.t -> 'a t
+
+    val stop : 'a t
+
+    val trap : Trap.t -> 'a t
+
+    val thread : thread t
+
+    val yield : unit t
+
+    val solver : Solver.t t
+
+    val with_thread : (thread -> 'a) -> 'a t
+
+    val set_thread : thread -> unit t
+
+    val modify_thread : (thread -> thread) -> unit t
+
+    (*
+       Indicates a possible choice between two values. Thread duplication
+       is already handled by choose and should not be done before by the caller.
+    *)
+    val choose : 'a t -> 'a t -> 'a t
+
+    type 'a run_result = ('a eval * thread) Seq.t
+
+    val run :
+         workers:int
+      -> Smtml.Solver_dispatcher.solver_type
+      -> 'a t
+      -> thread
+      -> callback:('a eval * thread -> unit)
+      -> callback_init:(unit -> unit)
+      -> callback_end:(unit -> unit)
+      -> unit Domain.t array
+  end = struct
+    include Eval
+
+    type 'a t = ('a, Thread.t) Eval.t
+
+    (*
        Here we define functions to seamlessly
        operate on the three monads layers
     *)
 
-  let lift_schedulable (v : ('a, _) Schedulable.t) : 'a t = lift (State.lift v)
+    let lift_schedulable (v : ('a, _) Schedulable.t) : 'a t =
+      let v = State.lift v in
+      lift v
 
-  let with_thread f = lift (State.with_state (fun st -> (f st, st)))
+    let with_thread (f : Thread.t -> 'a) : 'a t =
+      let x = State.with_state (fun st -> (f st, st)) in
+      lift x
 
-  let thread = with_thread Fun.id
+    let thread = with_thread Fun.id
 
-  let modify_thread f = lift (State.modify_state f)
+    let modify_thread f = lift (State.modify_state f)
 
-  let set_thread st = modify_thread (Fun.const st)
+    let set_thread st = modify_thread (Fun.const st)
 
-  let clone_thread = modify_thread Thread.clone
+    let clone_thread = modify_thread Thread.clone
 
-  let solver = lift_schedulable Schedulable.worker_local
+    let solver = lift_schedulable Schedulable.worker_local
 
-  let choose a b =
-    let a =
-      let* () = clone_thread in
-      a
-    in
-    let b =
-      let* () = clone_thread in
-      b
-    in
-    State.liftF2 Schedulable.choose a b
+    let choose a b =
+      let a =
+        let* () = clone_thread in
+        a
+      in
+      let b =
+        let* () = clone_thread in
+        b
+      in
+      State.liftF2 Schedulable.choose a b
 
-  let yield = lift_schedulable @@ Schedulable.yield Prio.default
+    let yield = lift_schedulable @@ Schedulable.yield Prio.default
 
-  let stop = lift_schedulable Schedulable.stop
+    let stop = lift_schedulable Schedulable.stop
 
-  type 'a run_result = ('a eval * Thread.t) Seq.t
+    type 'a run_result = ('a eval * Thread.t) Seq.t
 
-  let run ~workers solver t thread ~callback ~callback_init ~callback_end =
-    let open Scheduler in
-    let sched = init_scheduler () in
-    add_init_task sched (State.run t thread);
-    Array.init workers (fun _i ->
-        spawn_worker sched (Solver.fresh solver) callback callback_init
-          callback_end )
+    let run ~workers solver t thread ~callback ~callback_init ~callback_end =
+      let open Scheduler in
+      let sched = init_scheduler () in
+      add_init_task sched (State.run t thread);
+      Array.init workers (fun _i ->
+          spawn_worker sched (Solver.fresh solver) callback callback_init
+            callback_end )
 
-  let trap t =
-    let* thread in
-    let* solver in
-    let pc = Thread.pc thread in
-    let symbols = Thread.symbols_set thread |> Option.some in
-    let model = Solver.model solver ~symbols ~pc in
-    State.return (ETrap (t, model))
+    let trap t =
+      let* thread in
+      let* solver in
+      let pc = Thread.pc thread in
+      let symbols = Thread.symbols_set thread |> Option.some in
+      let model = Solver.model solver ~symbols ~pc in
+      State.return (ETrap (t, model))
 
-  let assertion_fail c model = State.return (EAssert (c, model))
+    let assertion_fail c model = State.return (EAssert (c, model))
+  end
 end
 
 (*
     We can now use CoreImpl only through its exposed signature which
     maintains all invariants.
   *)
-
-include CoreImpl
-
-let add_pc (c : Symbolic_value.vbool) =
-  match Smtml.Expr.view c with
-  | Val True -> return ()
-  | Val False -> stop
-  | _ ->
+module Make (Thread : Thread.S) = struct
+  include CoreImpl.Make (Thread)
+
+  let add_pc (c : Symbolic_value.vbool) =
+    match Smtml.Expr.view c with
+    | Val True -> return ()
+    | Val False -> stop
+    | _ ->
+      let* thread in
+      let new_thread = Thread.add_pc thread c in
+      set_thread new_thread
+  [@@inline]
+
+  let add_breadcrumb crumb =
+    modify_thread (fun t -> Thread.add_breadcrumb t crumb)
+
+  let with_new_symbol ty f =
     let* thread in
-    let new_thread = Thread.add_pc thread c in
-    set_thread new_thread
-[@@inline]
-
-let add_breadcrumb crumb =
-  modify_thread (fun t -> Thread.add_breadcrumb t crumb)
-
-let with_new_symbol ty f =
-  let* thread in
-  let n = Thread.symbols thread in
-  let sym = Fmt.kstr (Smtml.Symbol.make ty) "symbol_%d" n in
-  let+ () =
-    modify_thread (fun thread ->
-        let thread = Thread.add_symbol thread sym in
-        Thread.incr_symbols thread )
-  in
-  f sym
+    let n = Thread.symbols thread in
+    let sym = Fmt.kstr (Smtml.Symbol.make ty) "symbol_%d" n in
+    let+ () =
+      modify_thread (fun thread ->
+          let thread = Thread.add_symbol thread sym in
+          Thread.incr_symbols thread )
+    in
+    f sym
 
-(*
+  (*
     Yielding is currently done each time the solver is about to be called,
     in check_reachability and get_model.
   *)
-let check_reachability =
-  let* () = yield in
-  let* thread in
-  let* solver in
-  let pc = Thread.pc thread in
-  match Solver.check solver pc with
-  | `Sat -> return ()
-  | `Unsat | `Unknown -> stop
-
-let get_model_or_stop symbol =
-  let* () = yield in
-  let* solver in
-  let+ thread in
-  let pc = Thread.pc thread in
-  match Solver.check solver pc with
-  | `Unsat | `Unknown -> stop
-  | `Sat -> begin
-    let symbols = [ symbol ] |> Option.some in
-    let model = Solver.model solver ~symbols ~pc in
-    match Smtml.Model.evaluate model symbol with
-    | None ->
-      Fmt.failwith
-        "Unreachable: The model exists so this symbol should evaluate"
-    | Some v -> return v
-  end
+  let check_reachability =
+    let* () = yield in
+    let* thread in
+    let* solver in
+    let pc = Thread.pc thread in
+    match Solver.check solver pc with
+    | `Sat -> return ()
+    | `Unsat | `Unknown -> stop
 
-let select_inner ~explore_first (cond : Symbolic_value.vbool) =
-  let v = Smtml.Expr.simplify cond in
-  match Smtml.Expr.view v with
-  | Val True -> return true
-  | Val False -> return false
-  | Val (Num (I32 _)) -> Fmt.failwith "unreachable (type error)"
-  | _ ->
-    let true_branch =
-      let* () = add_pc v in
-      let* () = add_breadcrumb 1l in
-      let+ () = check_reachability in
-      true
-    in
-    let false_branch =
-      let* () = add_pc (Symbolic_value.Bool.not v) in
-      let* () = add_breadcrumb 0l in
-      let+ () = check_reachability in
-      false
-    in
-    if explore_first then choose true_branch false_branch
-    else choose false_branch true_branch
-[@@inline]
-
-let select (cond : Symbolic_value.vbool) = select_inner cond ~explore_first:true
-[@@inline]
-
-let summary_symbol (e : Smtml.Expr.t) =
-  let* thread in
-  match Smtml.Expr.view e with
-  | Symbol sym -> return (None, sym)
-  | _ ->
-    let num_symbols = Thread.symbols thread in
-    let+ () = modify_thread Thread.incr_symbols in
-    let sym_name = Fmt.str "choice_i32_%i" num_symbols in
-    let sym_type = Smtml.Ty.Ty_bitv 32 in
-    let sym = Smtml.Symbol.make sym_type sym_name in
-    let assign = Smtml.Expr.(relop Ty_bool Eq (mk_symbol sym) e) in
-    (Some assign, sym)
-
-let select_i32 (i : Symbolic_value.int32) =
-  let sym_int = Smtml.Expr.simplify i in
-  match Smtml.Expr.view sym_int with
-  | Val (Num (I32 i)) -> return i
-  | _ ->
-    let* assign, symbol = summary_symbol sym_int in
-    let* () =
-      match assign with Some assign -> add_pc assign | None -> return ()
-    in
-    let rec generator () =
-      let* possible_value = get_model_or_stop symbol in
-      let* possible_value in
-      let i =
-        match possible_value with
-        | Smtml.Value.Num (I32 i) -> i
-        | _ -> Fmt.failwith "Unreachable: found symbol must be a value"
-      in
-      let s = Smtml.Expr.mk_symbol symbol in
-      let this_value_cond =
-        let open Smtml.Expr in
-        Bitv.I32.(s = v i)
-      in
-      let not_this_value_cond =
-        let open Smtml.Expr in
-        (* != is **not** the physical inequality here *)
-        Bitv.I32.(s != v i)
-      in
-      let this_val_branch =
-        let* () = add_breadcrumb i in
-        let+ () = add_pc this_value_cond in
-        i
+  let get_model_or_stop symbol =
+    let* () = yield in
+    let* solver in
+    let+ thread in
+    let pc = Thread.pc thread in
+    match Solver.check solver pc with
+    | `Unsat | `Unknown -> stop
+    | `Sat -> begin
+      let symbols = [ symbol ] |> Option.some in
+      let model = Solver.model solver ~symbols ~pc in
+      match Smtml.Model.evaluate model symbol with
+      | None ->
+        Fmt.failwith
+          "Unreachable: The model exists so this symbol should evaluate"
+      | Some v -> return v
+    end
+
+  let select_inner ~explore_first (cond : Symbolic_value.vbool) =
+    let v = Smtml.Expr.simplify cond in
+    match Smtml.Expr.view v with
+    | Val True -> return true
+    | Val False -> return false
+    | Val (Num (I32 _)) -> Fmt.failwith "unreachable (type error)"
+    | _ ->
+      let true_branch =
+        let* () = add_pc v in
+        let* () = add_breadcrumb 1l in
+        let+ () = check_reachability in
+        true
       in
-      let not_this_val_branch =
-        let* () = add_pc not_this_value_cond in
-        generator ()
+      let false_branch =
+        let* () = add_pc (Symbolic_value.Bool.not v) in
+        let* () = add_breadcrumb 0l in
+        let+ () = check_reachability in
+        false
       in
-      choose this_val_branch not_this_val_branch
-    in
-    generator ()
+      if explore_first then choose true_branch false_branch
+      else choose false_branch true_branch
+  [@@inline]
+
+  let select (cond : Symbolic_value.vbool) =
+    select_inner cond ~explore_first:true
+  [@@inline]
 
-let assertion c =
-  let* assertion_true = select_inner c ~explore_first:false in
-  if assertion_true then return ()
-  else
+  let summary_symbol (e : Smtml.Expr.t) =
     let* thread in
-    let* solver in
-    let symbols = Thread.symbols_set thread |> Option.some in
-    let pc = Thread.pc thread in
-    let model = Solver.model ~symbols ~pc solver in
-    assertion_fail c model
+    match Smtml.Expr.view e with
+    | Symbol sym -> return (None, sym)
+    | _ ->
+      let num_symbols = Thread.symbols thread in
+      let+ () = modify_thread Thread.incr_symbols in
+      let sym_name = Fmt.str "choice_i32_%i" num_symbols in
+      let sym_type = Smtml.Ty.Ty_bitv 32 in
+      let sym = Smtml.Symbol.make sym_type sym_name in
+      let assign = Smtml.Expr.(relop Ty_bool Eq (mk_symbol sym) e) in
+      (Some assign, sym)
+
+  let select_i32 (i : Symbolic_value.int32) =
+    let sym_int = Smtml.Expr.simplify i in
+    match Smtml.Expr.view sym_int with
+    | Val (Num (I32 i)) -> return i
+    | _ ->
+      let* assign, symbol = summary_symbol sym_int in
+      let* () =
+        match assign with Some assign -> add_pc assign | None -> return ()
+      in
+      let rec generator () =
+        let* possible_value = get_model_or_stop symbol in
+        let* possible_value in
+        let i =
+          match possible_value with
+          | Smtml.Value.Num (I32 i) -> i
+          | _ -> Fmt.failwith "Unreachable: found symbol must be a value"
+        in
+        let s = Smtml.Expr.mk_symbol symbol in
+        let this_value_cond =
+          let open Smtml.Expr in
+          Bitv.I32.(s = v i)
+        in
+        let not_this_value_cond =
+          let open Smtml.Expr in
+          (* != is **not** the physical inequality here *)
+          Bitv.I32.(s != v i)
+        in
+        let this_val_branch =
+          let* () = add_breadcrumb i in
+          let+ () = add_pc this_value_cond in
+          i
+        in
+        let not_this_val_branch =
+          let* () = add_pc not_this_value_cond in
+          generator ()
+        in
+        choose this_val_branch not_this_val_branch
+      in
+      generator ()
+
+  let assertion c =
+    let* assertion_true = select_inner c ~explore_first:false in
+    if assertion_true then return ()
+    else
+      let* thread in
+      let* solver in
+      let symbols = Thread.symbols_set thread |> Option.some in
+      let pc = Thread.pc thread in
+      let model = Solver.model ~symbols ~pc solver in
+      assertion_fail c model
+end
diff --git a/src/symbolic/symbolic_choice.mli b/src/symbolic/symbolic_choice.mli
index c52a97c0d..248f3fa72 100644
--- a/src/symbolic/symbolic_choice.mli
+++ b/src/symbolic/symbolic_choice.mli
@@ -2,25 +2,5 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-type 'a eval = private
-  | EVal of 'a
-  | ETrap of Trap.t * Smtml.Model.t
-  | EAssert of Smtml.Expr.t * Smtml.Model.t
-
-include
-  Choice_intf.Complete
-    with type thread := Thread.t
-     and type 'a run_result = ('a eval * Thread.t) Seq.t
-     and module V := Symbolic_value
-
-val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
-
-val run :
-     workers:int
-  -> Smtml.Solver_dispatcher.solver_type
-  -> 'a t
-  -> Thread.t
-  -> callback:('a eval * Thread.t -> unit)
-  -> callback_init:(unit -> unit)
-  -> callback_end:(unit -> unit)
-  -> unit Domain.t array
+(** @inline *)
+include Symbolic_choice_intf.Intf
diff --git a/src/symbolic/symbolic_choice_minimalist.ml b/src/symbolic/symbolic_choice_minimalist.ml
index 24e55a32a..9dcddac6e 100644
--- a/src/symbolic/symbolic_choice_minimalist.ml
+++ b/src/symbolic/symbolic_choice_minimalist.ml
@@ -4,64 +4,70 @@
 
 open Symbolic_value
 
-type err =
-  | Assert_fail
-  | Trap of Trap.t
+module Make (Thread : Thread.S) = struct
+  type err =
+    | Assert_fail
+    | Trap of Trap.t
 
-type 'a t =
-  | M of (Thread.t -> Solver.t -> ('a, err) Prelude.Result.t * Thread.t)
-[@@unboxed]
+  type 'a t =
+    | M of (Thread.t -> Solver.t -> ('a, err) Prelude.Result.t * Thread.t)
+  [@@unboxed]
 
-type 'a run_result = ('a, err) Prelude.Result.t * Thread.t
+  type 'a run_result = ('a, err) Prelude.Result.t * Thread.t
 
-let return v = M (fun t _sol -> (Ok v, t))
+  let return v = M (fun t _sol -> (Ok v, t))
 
-let run (M v) st s : _ run_result = v st s
+  let run (M v) st s : _ run_result = v st s
 
-let bind v f =
-  M
-    (fun init_s sol ->
-      let v_final, tmp_st = run v init_s sol in
-      match v_final with
-      | Ok v_final -> run (f v_final) tmp_st sol
-      | Error _ as e -> (e, tmp_st) )
+  let bind v f =
+    M
+      (fun init_s sol ->
+        let v_final, tmp_st = run v init_s sol in
+        match v_final with
+        | Ok v_final -> run (f v_final) tmp_st sol
+        | Error _ as e -> (e, tmp_st) )
 
-let ( let* ) = bind
+  let ( let* ) = bind
 
-let map v f =
-  let* v in
-  return (f v)
+  let map v f =
+    let* v in
+    return (f v)
 
-let ( let+ ) = map
+  let ( let+ ) = map
 
-let select (vb : vbool) =
-  let v = Smtml.Expr.simplify vb in
-  match Smtml.Expr.view v with
-  | Val True -> return true
-  | Val False -> return false
-  | _ -> Fmt.failwith "%a" Smtml.Expr.pp v
+  let select (vb : vbool) =
+    let v = Smtml.Expr.simplify vb in
+    match Smtml.Expr.view v with
+    | Val True -> return true
+    | Val False -> return false
+    | _ -> Fmt.failwith "%a" Smtml.Expr.pp v
 
-let select_i32 (i : int32) =
-  let v = Smtml.Expr.simplify i in
-  match Smtml.Expr.view v with
-  | Val (Num (I32 i)) -> return i
-  | _ -> assert false
+  let select_i32 (i : int32) =
+    let v = Smtml.Expr.simplify i in
+    match Smtml.Expr.view v with
+    | Val (Num (I32 i)) -> return i
+    | _ -> assert false
 
-let trap t = M (fun th _sol -> (Error (Trap t), th))
+  let trap t = M (fun th _sol -> (Error (Trap t), th))
 
-let assertion (vb : vbool) =
-  let v = Smtml.Expr.simplify vb in
-  match Smtml.Expr.view v with
-  | Val True -> return ()
-  | Val False -> M (fun th _sol -> (Error Assert_fail, th))
-  | _ -> assert false
+  let assertion (vb : vbool) =
+    let v = Smtml.Expr.simplify vb in
+    match Smtml.Expr.view v with
+    | Val True -> return ()
+    | Val False -> M (fun th _sol -> (Error Assert_fail, th))
+    | _ -> assert false
 
-let with_thread f = M (fun st _sol -> (Ok (f st), st))
+  let with_thread f = M (fun st _sol -> (Ok (f st), st))
 
-let thread = M (fun st _sol -> (Ok st, st))
+  let thread = M (fun st _sol -> (Ok st, st))
 
-let solver = M (fun st sol -> (Ok sol, st))
+  let solver = M (fun st sol -> (Ok sol, st))
 
-let add_pc (_vb : vbool) = return ()
+  let add_pc (_vb : vbool) = return ()
 
-let run ~workers:_ solver t thread = run t thread (Solver.fresh solver ())
+  let run ~workers:_ solver t thread = run t thread (Solver.fresh solver ())
+
+  let lift_mem _ = assert false
+end
+
+include Make (Thread_with_memory)
diff --git a/src/symbolic/symbolic_choice_minimalist.mli b/src/symbolic/symbolic_choice_minimalist.mli
index a4a264317..d6f3cb91f 100644
--- a/src/symbolic/symbolic_choice_minimalist.mli
+++ b/src/symbolic/symbolic_choice_minimalist.mli
@@ -8,13 +8,13 @@ type err = private
 
 include
   Choice_intf.Complete
-    with type thread := Thread.t
-     and type 'a run_result = ('a, err) Prelude.Result.t * Thread.t
+    with type thread := Thread_with_memory.t
+     and type 'a run_result = ('a, err) Prelude.Result.t * Thread_with_memory.t
      and module V := Symbolic_value
 
 val run :
      workers:int
   -> Smtml.Solver_dispatcher.solver_type
   -> 'a t
-  -> Thread.t
+  -> Thread_with_memory.t
   -> 'a run_result
diff --git a/src/symbolic/symbolic_choice_with_memory.ml b/src/symbolic/symbolic_choice_with_memory.ml
new file mode 100644
index 000000000..d143f5d0b
--- /dev/null
+++ b/src/symbolic/symbolic_choice_with_memory.ml
@@ -0,0 +1,9 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+include Symbolic_choice.Make (Thread_with_memory)
+
+let lift_mem (mem_op : 'a Symbolic_choice_without_memory.t) : 'a t =
+  Symbolic_choice.CoreImpl.State.project_state Thread_with_memory.project
+    Thread_with_memory.restore mem_op
diff --git a/src/symbolic/symbolic_choice_with_memory.mli b/src/symbolic/symbolic_choice_with_memory.mli
new file mode 100644
index 000000000..dfdf98570
--- /dev/null
+++ b/src/symbolic/symbolic_choice_with_memory.mli
@@ -0,0 +1,14 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+include
+  Symbolic_choice_intf.S
+    with type 'a t =
+      ( 'a Symbolic_choice_intf.eval
+      , Thread_with_memory.t )
+      Symbolic_choice.CoreImpl.State.t
+     and type thread := Thread_with_memory.t
+     and module V := Symbolic_value
+
+val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
diff --git a/src/symbolic/symbolic_choice_without_memory.ml b/src/symbolic/symbolic_choice_without_memory.ml
new file mode 100644
index 000000000..5041426ce
--- /dev/null
+++ b/src/symbolic/symbolic_choice_without_memory.ml
@@ -0,0 +1,5 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+include Symbolic_choice.Make (Thread_without_memory)
diff --git a/src/symbolic/symbolic_choice_without_memory.mli b/src/symbolic/symbolic_choice_without_memory.mli
new file mode 100644
index 000000000..422b6cd55
--- /dev/null
+++ b/src/symbolic/symbolic_choice_without_memory.mli
@@ -0,0 +1,12 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+include
+  Symbolic_choice_intf.S
+    with type 'a t =
+      ( 'a Symbolic_choice_intf.eval
+      , Thread_without_memory.t )
+      Symbolic_choice.CoreImpl.State.t
+     and type thread := Thread_without_memory.t
+     and module V := Symbolic_value
diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml
index fd12d28ff..030156750 100644
--- a/src/symbolic/symbolic_wasm_ffi.ml
+++ b/src/symbolic/symbolic_wasm_ffi.ml
@@ -3,7 +3,7 @@
 (* Written by the Owi programmers *)
 
 module Expr = Smtml.Expr
-module Choice = Symbolic_choice
+module Choice = Symbolic_choice_with_memory
 module Memory = Symbolic_memory
 
 (* The constraint is used here to make sure we don't forget to define one of the expected FFI functions, this whole file is further constrained such that if one function of M is unused in the FFI module below, an error will be displayed *)
diff --git a/src/symbolic/thread.ml b/src/symbolic/thread.ml
index 0f16d4b63..979f4fd01 100644
--- a/src/symbolic/thread.ml
+++ b/src/symbolic/thread.ml
@@ -1,53 +1,64 @@
 (* SPDX-License-Identifier: AGPL-3.0-or-later *)
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
+include Thread_intf
 
-type t =
-  { symbols : int
-  ; symbol_set : Smtml.Symbol.t list
-  ; pc : Symbolic_value.vbool list
-  ; memories : Symbolic_memory.collection
-  ; tables : Symbolic_table.collection
-  ; globals : Symbolic_global.collection
-      (** Breadcrumbs represent the list of choices that were made so far. They
-          identify one given symbolic execution trace. *)
-  ; breadcrumbs : int32 list
-  }
+module Make (Symbolic_memory : M) :
+  S with type Memory.collection = Symbolic_memory.collection = struct
+  module Memory : M with type collection = Symbolic_memory.collection =
+    Symbolic_memory
 
-let symbols t = t.symbols
+  type t =
+    { symbols : int
+    ; symbol_set : Smtml.Symbol.t list
+    ; pc : Symbolic_value.vbool list
+    ; memories : Memory.collection
+    ; tables : Symbolic_table.collection
+    ; globals : Symbolic_global.collection
+        (** Breadcrumbs represent the list of choices that were made so far.
+            They identify one given symbolic execution trace. *)
+    ; breadcrumbs : int32 list
+    }
 
-let pc t = t.pc
+  let create symbols symbol_set pc memories tables globals breadcrumbs =
+    { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs }
 
-let memories t = t.memories
+  let init () =
+    let symbols = 0 in
+    let symbol_set = [] in
+    let pc = [] in
+    let memories = Memory.init () in
+    let tables = Symbolic_table.init () in
+    let globals = Symbolic_global.init () in
+    let breadcrumbs = [] in
+    create symbols symbol_set pc memories tables globals breadcrumbs
 
-let tables t = t.tables
+  let symbols t = t.symbols
 
-let globals t = t.globals
+  let symbols_set t = t.symbol_set
 
-let breadcrumbs t = t.breadcrumbs
+  let pc t = t.pc
 
-let symbols_set t = t.symbol_set
+  let memories t = t.memories
 
-let add_symbol t s = { t with symbol_set = s :: t.symbol_set }
+  let tables t = t.tables
 
-let add_pc t c = { t with pc = c :: t.pc }
+  let globals t = t.globals
 
-let add_breadcrumb t crumb = { t with breadcrumbs = crumb :: t.breadcrumbs }
+  let breadcrumbs t = t.breadcrumbs
 
-let incr_symbols t = { t with symbols = succ t.symbols }
+  let add_symbol t s = { t with symbol_set = s :: t.symbol_set }
 
-let create () =
-  { symbols = 0
-  ; symbol_set = []
-  ; pc = []
-  ; memories = Symbolic_memory.init ()
-  ; tables = Symbolic_table.init ()
-  ; globals = Symbolic_global.init ()
-  ; breadcrumbs = []
-  }
+  let add_pc t c = { t with pc = c :: t.pc }
 
-let clone { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs } =
-  let memories = Symbolic_memory.clone memories in
-  let tables = Symbolic_table.clone tables in
-  let globals = Symbolic_global.clone globals in
-  { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs }
+  let add_breadcrumb t crumb = { t with breadcrumbs = crumb :: t.breadcrumbs }
+
+  let incr_symbols t = { t with symbols = succ t.symbols }
+
+  let clone { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs }
+      =
+    let memories = Memory.clone memories in
+    let tables = Symbolic_table.clone tables in
+    let globals = Symbolic_global.clone globals in
+    { symbols; symbol_set; pc; memories; tables; globals; breadcrumbs }
+end
diff --git a/src/symbolic/thread.mli b/src/symbolic/thread.mli
index d24d7b359..53aab072b 100644
--- a/src/symbolic/thread.mli
+++ b/src/symbolic/thread.mli
@@ -2,30 +2,5 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-type t
-
-val pc : t -> Symbolic_value.vbool list
-
-val memories : t -> Symbolic_memory.collection
-
-val tables : t -> Symbolic_table.collection
-
-val globals : t -> Symbolic_global.collection
-
-val breadcrumbs : t -> int32 list
-
-val symbols_set : t -> Smtml.Symbol.t list
-
-val symbols : t -> int
-
-val create : unit -> t
-
-val clone : t -> t
-
-val add_pc : t -> Symbolic_value.vbool -> t
-
-val add_breadcrumb : t -> int32 -> t
-
-val add_symbol : t -> Smtml.Symbol.t -> t
-
-val incr_symbols : t -> t
+(** @inline *)
+include Thread_intf.Intf
diff --git a/src/symbolic/thread_with_memory.ml b/src/symbolic/thread_with_memory.ml
new file mode 100644
index 000000000..86646e600
--- /dev/null
+++ b/src/symbolic/thread_with_memory.ml
@@ -0,0 +1,33 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+include Thread.Make (Symbolic_memory)
+
+let project (th : t) : Thread_without_memory.t * _ =
+  let projected =
+    let symbols = symbols th in
+    let symbols_set = symbols_set th in
+    let pc = pc th in
+    let memories = Thread_without_memory.Memory.init () in
+    let tables = tables th in
+    let globals = globals th in
+    let breadcrumbs = breadcrumbs th in
+    Thread_without_memory.create symbols symbols_set pc memories tables globals
+      breadcrumbs
+  in
+  let backup = memories th in
+  (projected, backup)
+
+let restore backup th =
+  let symbols = Thread_without_memory.symbols th in
+  let symbols_set = Thread_without_memory.symbols_set th in
+  let pc = Thread_without_memory.pc th in
+  let memories =
+    if Thread_without_memory.memories th then Symbolic_memory.clone backup
+    else backup
+  in
+  let tables = Thread_without_memory.tables th in
+  let globals = Thread_without_memory.globals th in
+  let breadcrumbs = Thread_without_memory.breadcrumbs th in
+  create symbols symbols_set pc memories tables globals breadcrumbs
diff --git a/src/symbolic/thread_with_memory.mli b/src/symbolic/thread_with_memory.mli
new file mode 100644
index 000000000..0e93de7a9
--- /dev/null
+++ b/src/symbolic/thread_with_memory.mli
@@ -0,0 +1,10 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+(** @inline *)
+include Thread.S with type Memory.collection = Symbolic_memory.collection
+
+val project : t -> Thread_without_memory.t * Memory.collection
+
+val restore : Memory.collection -> Thread_without_memory.t -> t
diff --git a/src/symbolic/thread_without_memory.ml b/src/symbolic/thread_without_memory.ml
new file mode 100644
index 000000000..7c3b6a9db
--- /dev/null
+++ b/src/symbolic/thread_without_memory.ml
@@ -0,0 +1,11 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+include Thread.Make (struct
+  type collection = bool
+
+  let init () = false
+
+  let clone _ = true
+end)
diff --git a/src/symbolic/thread_without_memory.mli b/src/symbolic/thread_without_memory.mli
new file mode 100644
index 000000000..f385f9e7e
--- /dev/null
+++ b/src/symbolic/thread_without_memory.mli
@@ -0,0 +1,6 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+(** @inline *)
+include Thread.S with type Memory.collection = bool
diff --git a/test/fuzz/interprets.ml b/test/fuzz/interprets.ml
index 91e2b3f48..6a6b2457b 100644
--- a/test/fuzz/interprets.ml
+++ b/test/fuzz/interprets.ml
@@ -82,7 +82,7 @@ module Owi_symbolic : INTERPRET = struct
     let regular = Symbolic.convert_module_to_run_minimalist regular in
     timeout_call_run (fun () ->
         let c = Interpret.SymbolicM.modul link_state.envs regular in
-        let init_thread : Thread.t = Thread.create () in
+        let init_thread = Thread_with_memory.init () in
         let res, _ =
           Symbolic_choice_minimalist.run ~workers:dummy_workers_count
             Smtml.Solver_dispatcher.Z3_solver c init_thread