diff --git a/src/dune b/src/dune
index d95dc021c..3b449742b 100644
--- a/src/dune
+++ b/src/dune
@@ -67,6 +67,9 @@
   symbolic_choice_without_memory
   symbolic_global
   symbolic_memory
+  symbolic_memory_concretizing
+  symbolic_memory_intf
+  symbolic_memory_make
   symbolic_table
   symbolic_value
   symbolic_wasm_ffi
diff --git a/src/intf/symbolic_memory_intf.ml b/src/intf/symbolic_memory_intf.ml
new file mode 100644
index 000000000..6d690fd8f
--- /dev/null
+++ b/src/intf/symbolic_memory_intf.ml
@@ -0,0 +1,138 @@
+module type M = sig
+  type t
+
+  type address
+
+  val address : Smtml.Expr.t -> address Symbolic_choice_without_memory.t
+
+  val address_i32 : Int32.t -> address
+
+  val make : unit -> t
+
+  val clone : t -> t
+
+  val loadn : t -> address -> int -> Smtml.Expr.t
+
+  val storen : t -> address -> Smtml.Expr.t -> int -> unit
+
+  val validate_address :
+       t
+    -> Smtml.Expr.t
+    -> (Smtml.Expr.t, Trap.t) result Symbolic_choice_without_memory.t
+
+  val realloc :
+       t
+    -> ptr:Smtml.Expr.t
+    -> size:Smtml.Expr.t
+    -> Smtml.Expr.t Symbolic_choice_without_memory.t
+
+  val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
+end
+
+module type S = sig
+  type t
+
+  type collection
+
+  val init : unit -> collection
+
+  val clone : collection -> collection
+
+  val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
+
+  (* val check_within_bounds : *)
+  (*   t -> Smtml.Expr.t -> (Smtml.Expr.t * Symbolic_value.int32, Trap.t) result *)
+
+  val realloc :
+       t
+    -> ptr:Smtml.Expr.t
+    -> size:Smtml.Expr.t
+    -> Smtml.Expr.t Symbolic_choice_without_memory.t
+
+  val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
+
+  val load_8_s :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_8_u :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_16_s :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_16_u :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_32 :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val load_64 :
+    t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+  val store_8 :
+       t
+    -> addr:Smtml.Expr.t
+    -> Smtml.Expr.t
+    -> unit Symbolic_choice_without_memory.t
+
+  val store_16 :
+       t
+    -> addr:Smtml.Expr.t
+    -> Smtml.Expr.t
+    -> unit Symbolic_choice_without_memory.t
+
+  val store_32 :
+       t
+    -> addr:Smtml.Expr.t
+    -> Smtml.Expr.t
+    -> unit Symbolic_choice_without_memory.t
+
+  val store_64 :
+       t
+    -> addr:Smtml.Expr.t
+    -> Smtml.Expr.t
+    -> unit Symbolic_choice_without_memory.t
+
+  val grow : t -> Smtml.Expr.t -> unit
+
+  val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
+
+  val blit :
+       t
+    -> src:Smtml.Expr.t
+    -> dst:Smtml.Expr.t
+    -> len:Smtml.Expr.t
+    -> Smtml.Expr.t
+
+  val blit_string :
+       t
+    -> string
+    -> src:Smtml.Expr.t
+    -> dst:Smtml.Expr.t
+    -> len:Smtml.Expr.t
+    -> Smtml.Expr.t
+
+  val size : t -> Smtml.Expr.t
+
+  val size_in_pages : t -> Smtml.Expr.t
+
+  val get_limit_max : t -> Smtml.Expr.t option
+
+  module ITbl : sig
+    type 'a t
+
+    type key
+
+    val iter : (key -> 'a -> unit) -> 'a t -> unit
+  end
+
+  val iter : (t ITbl.t -> unit) -> collection -> unit
+end
+
+module type Intf = sig
+  module type M = M
+
+  module type S = S
+
+  module Make (_ : M) : S
+end
diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml
index c33009e98..aab9ecc96 100644
--- a/src/symbolic/symbolic.ml
+++ b/src/symbolic/symbolic.ml
@@ -3,15 +3,15 @@
 (* Written by the Owi programmers *)
 
 module MakeP
-    (Thread : Thread.S with type Memory.collection = Symbolic_memory.collection)
+    (Memory : Symbolic_memory_intf.S)
+    (Thread : Thread.S with type Memory.collection = Memory.collection)
     (Choice : Choice_intf.Complete
                 with module V := Symbolic_value
                  and type thread := Thread.t) =
 struct
   module Value = Symbolic_value
   module Choice = Choice
-  module Extern_func =
-    Concrete_value.Make_extern_func (Value) (Choice) (Symbolic_memory)
+  module Extern_func = Concrete_value.Make_extern_func (Value) (Choice) (Memory)
   module Global = Symbolic_global
   module Table = Symbolic_table
 
@@ -44,60 +44,27 @@ struct
   end
 
   module Memory = struct
-    include Symbolic_memory
+    include Memory
 
-    let concretise (a : Smtml.Expr.t) : Smtml.Expr.t Choice.t =
-      let open Choice in
-      let open Smtml in
-      match Expr.view a with
-      (* Avoid unecessary re-hashconsing and allocation when the value
-         is already concrete. *)
-      | Val _ | Ptr { offset = { node = Val _; _ }; _ } -> return a
-      | Ptr { base; offset } ->
-        let+ offset = select_i32 offset in
-        Expr.ptr base (Symbolic_value.const_i32 offset)
-      | _ ->
-        let+ v = select_i32 a in
-        Symbolic_value.const_i32 v
-
-    let check_within_bounds m a =
-      match check_within_bounds m a with
-      | Error t -> Choice.trap t
-      | Ok (cond, ptr) ->
-        let open Choice in
-        let* out_of_bounds = select cond in
-        if out_of_bounds then trap Trap.Memory_heap_buffer_overflow
-        else return ptr
-
-    let with_concrete (m : t) a f : 'a Choice.t =
-      let open Choice in
-      let* addr = concretise a in
-      let+ ptr = check_within_bounds m addr in
-      f m ptr
-
-    let load_8_s m a = with_concrete m a load_8_s
+    let load_8_s m a = Choice.lift_mem @@ load_8_s m a
 
-    let load_8_u m a = with_concrete m a load_8_u
+    let load_8_u m a = Choice.lift_mem @@ load_8_u m a
 
-    let load_16_s m a = with_concrete m a load_16_s
+    let load_16_s m a = Choice.lift_mem @@ load_16_s m a
 
-    let load_16_u m a = with_concrete m a load_16_u
+    let load_16_u m a = Choice.lift_mem @@ load_16_u m a
 
-    let load_32 m a = with_concrete m a load_32
+    let load_32 m a = Choice.lift_mem @@ load_32 m a
 
-    let load_64 m a = with_concrete m a load_64
+    let load_64 m a = Choice.lift_mem @@ load_64 m a
 
-    let store_8 m ~addr v =
-      with_concrete m addr (fun m addr -> store_8 m ~addr v)
+    let store_8 m ~addr v = Choice.lift_mem @@ store_8 m ~addr v
 
-    let store_16 m ~addr v =
-      with_concrete m addr (fun m addr -> store_16 m ~addr v)
+    let store_16 m ~addr v = Choice.lift_mem @@ store_16 m ~addr v
 
-    let store_32 m ~addr v =
-      with_concrete m addr (fun m addr -> store_32 m ~addr v)
+    let store_32 m ~addr v = Choice.lift_mem @@ store_32 m ~addr v
 
-    let store_64 m ~addr v =
-      with_concrete m addr (fun m addr -> store_64 m ~addr v)
+    let store_64 m ~addr v = Choice.lift_mem @@ store_64 m ~addr v
   end
 
   module Data = struct
@@ -115,7 +82,7 @@ struct
       let orig_mem = Link_env.get_memory env id in
       let f (t : thread) =
         let memories = Thread.memories t in
-        Symbolic_memory.get_memory (Link_env.id env) orig_mem memories id
+        Memory.get_memory (Link_env.id env) orig_mem memories id
       in
       Choice.with_thread f
 
@@ -169,9 +136,11 @@ struct
 end
 
 module P =
-  MakeP [@inlined hint] (Thread_with_memory) (Symbolic_choice_with_memory)
+  MakeP [@inlined hint] (Symbolic_memory_concretizing) (Thread_with_memory)
+    (Symbolic_choice_with_memory)
 module M =
-  MakeP [@inlined hint] (Thread_with_memory) (Symbolic_choice_minimalist)
+  MakeP [@inlined hint] (Symbolic_memory_concretizing) (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_memory.ml b/src/symbolic/symbolic_memory.ml
index dca85d11c..56771af1f 100644
--- a/src/symbolic/symbolic_memory.ml
+++ b/src/symbolic/symbolic_memory.ml
@@ -197,7 +197,7 @@ let free m base =
     Fmt.failwith "Memory leak double free";
   Hashtbl.remove m.chunks base
 
-let replace_size m base size = Hashtbl.replace m.chunks base size
+let realloc m base size = Hashtbl.replace m.chunks base size
 
 module ITbl = Hashtbl.Make (struct
   include Int
diff --git a/src/symbolic/symbolic_memory.mli b/src/symbolic/symbolic_memory.mli
index 276272885..3c35719fb 100644
--- a/src/symbolic/symbolic_memory.mli
+++ b/src/symbolic/symbolic_memory.mli
@@ -15,7 +15,7 @@ val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
 val check_within_bounds :
   t -> Smtml.Expr.t -> (Smtml.Expr.t * Symbolic_value.int32, Trap.t) result
 
-val replace_size : t -> Int32.t -> Smtml.Expr.t -> unit
+val realloc : t -> Int32.t -> Smtml.Expr.t -> unit
 
 val free : t -> Int32.t -> unit
 
diff --git a/src/symbolic/symbolic_memory_concretizing.ml b/src/symbolic/symbolic_memory_concretizing.ml
new file mode 100644
index 000000000..19156eb66
--- /dev/null
+++ b/src/symbolic/symbolic_memory_concretizing.ml
@@ -0,0 +1,150 @@
+module Backend = struct
+  open Smtml
+
+  type address = Int32.t
+
+  type t =
+    { data : (address, Symbolic_value.int32) Hashtbl.t
+    ; parent : t option
+    ; chunks : (address, Symbolic_value.int32) Hashtbl.t
+    }
+
+  let make () =
+    { data = Hashtbl.create 16; parent = None; chunks = Hashtbl.create 16 }
+
+  let clone m =
+    (* TODO: Make chunk copying lazy *)
+    { data = Hashtbl.create 16
+    ; parent = Some m
+    ; chunks = Hashtbl.copy m.chunks
+    }
+
+  let address a =
+    let open Symbolic_choice_without_memory in
+    match Expr.view a with
+    | Val (Num (I32 i)) -> return i
+    | Ptr { base; offset } ->
+      select_i32 Symbolic_value.(I32.add (const_i32 base) offset)
+    | _ -> select_i32 a
+
+  let address_i32 a = a
+
+  let rec load_byte { parent; data; _ } a =
+    try Hashtbl.find data a
+    with Not_found -> (
+      match parent with
+      | None -> Expr.value (Num (I8 0))
+      | Some parent -> load_byte parent a )
+
+  (* TODO: don't rebuild so many values it generates unecessary hc lookups *)
+  let merge_extracts (e1, h, m1) (e2, m2, l) =
+    let ty = Expr.ty e1 in
+    if m1 = m2 && Expr.equal e1 e2 then
+      if h - l = Ty.size ty then e1 else Expr.make (Extract (e1, h, l))
+    else
+      Expr.(
+        make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) )
+
+  let concat ~msb ~lsb offset =
+    assert (offset > 0 && offset <= 8);
+    match (Expr.view msb, Expr.view lsb) with
+    | Val (Num (I8 i1)), Val (Num (I8 i2)) ->
+      Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
+    | Val (Num (I8 i1)), Val (Num (I32 i2)) ->
+      let offset = offset * 8 in
+      if offset < 32 then
+        Symbolic_value.const_i32
+          Int32.(logor (shl (of_int i1) (of_int offset)) i2)
+      else
+        let i1' = Int64.of_int i1 in
+        let i2' = Int64.of_int32 i2 in
+        Symbolic_value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
+    | Val (Num (I8 i1)), Val (Num (I64 i2)) ->
+      let offset = Int64.of_int (offset * 8) in
+      Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
+    | Extract (e1, h, m1), Extract (e2, m2, l) ->
+      merge_extracts (e1, h, m1) (e2, m2, l)
+    | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) ->
+      Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3)))
+    | _ -> Expr.make (Concat (msb, lsb))
+
+  let loadn m a n =
+    let rec loop addr size i acc =
+      if i = size then acc
+      else
+        let addr' = Int32.(add addr (of_int i)) in
+        let byte = load_byte m addr' in
+        loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
+    in
+    let v0 = load_byte m a in
+    loop a n 1 v0
+
+  let extract v pos =
+    match Expr.view v with
+    | Val (Num (I8 _)) -> v
+    | Val (Num (I32 i)) ->
+      let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
+      Expr.value (Num (I8 i'))
+    | Val (Num (I64 i)) ->
+      let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
+      Expr.value (Num (I8 i'))
+    | Cvtop
+        (_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
+    | Cvtop
+        (_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym))
+      ->
+      sym
+    | _ -> Expr.make (Extract (v, pos + 1, pos))
+
+  let storen m a v n =
+    for i = 0 to n - 1 do
+      let a' = Int32.add a (Int32.of_int i) in
+      let v' = extract v i in
+      Hashtbl.replace m.data a' v'
+    done
+
+  let validate_address m a =
+    let open Symbolic_choice_without_memory in
+    match Smtml.Expr.view a with
+    | Val (Num (I32 _)) -> return (Ok a) (* An i32 is a valid address *)
+    | Ptr { base; offset } -> (
+      let (* A pointer is valid if it's within bounds. *)
+      open Symbolic_value in
+      match Hashtbl.find m.chunks base with
+      | exception Not_found -> return (Error Trap.Memory_leak_use_after_free)
+      | size ->
+        let base = const_i32 base in
+        let ptr = I32.add base offset in
+        let+ is_out_of_bounds =
+          select (Bool.or_ (I32.lt ptr base) (I32.ge ptr (I32.add base size)))
+        in
+        if is_out_of_bounds then Error Trap.Memory_heap_buffer_overflow
+        else Ok a )
+    | _ ->
+      (* A symbolic expression should be a valid address *)
+      return (Ok a)
+
+  let ptr v =
+    let open Symbolic_choice_without_memory in
+    match Expr.view v with
+    | Ptr { base; _ } -> return base
+    | _ ->
+      Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v;
+      let* () = add_pc @@ Expr.value False in
+      assert false
+
+  let free m p =
+    let open Symbolic_choice_without_memory in
+    let+ base = ptr p in
+    if not @@ Hashtbl.mem m.chunks base then
+      Fmt.failwith "Memory leak double free";
+    Hashtbl.remove m.chunks base
+
+  let realloc m ~ptr ~size =
+    let open Symbolic_choice_without_memory in
+    let+ base = address ptr in
+    Hashtbl.replace m.chunks base size;
+    Expr.ptr base (Symbolic_value.const_i32 0l)
+end
+
+include Symbolic_memory_make.Make (Backend)
diff --git a/src/symbolic/symbolic_memory_concretizing.mli b/src/symbolic/symbolic_memory_concretizing.mli
new file mode 100644
index 000000000..629a8dd9f
--- /dev/null
+++ b/src/symbolic/symbolic_memory_concretizing.mli
@@ -0,0 +1,6 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+(** @inline *)
+include Symbolic_memory_intf.S
diff --git a/src/symbolic/symbolic_memory_make.ml b/src/symbolic/symbolic_memory_make.ml
new file mode 100644
index 000000000..88f9c2a4b
--- /dev/null
+++ b/src/symbolic/symbolic_memory_make.ml
@@ -0,0 +1,180 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+include Symbolic_memory_intf
+
+let page_size = Symbolic_value.const_i32 65_536l
+
+module Make (Backend : M) = struct
+  type t =
+    { data : Backend.t
+    ; mutable size : Symbolic_value.int32
+    }
+
+  let create size =
+    { data = Backend.make (); size = Symbolic_value.const_i32 size }
+
+  let i32 v =
+    match Smtml.Expr.view v with
+    | Val (Num (I32 i)) -> i
+    | _ ->
+      Log.err {|Unsupported symbolic value reasoning over "%a"|} Smtml.Expr.pp v
+
+  let grow m delta =
+    let old_size = Symbolic_value.I32.mul m.size page_size in
+    let new_size = Symbolic_value.I32.(div (add old_size delta) page_size) in
+    m.size <-
+      Symbolic_value.Bool.select_expr
+        (Symbolic_value.I32.gt new_size m.size)
+        ~if_true:new_size ~if_false:m.size
+
+  let size { size; _ } = Symbolic_value.I32.mul size page_size
+
+  let size_in_pages { size; _ } = size
+
+  let fill _ = assert false
+
+  let blit _ = assert false
+
+  let blit_string m str ~src ~dst ~len =
+    (* This function is only used in memory init so everything will be concrete *)
+    let str_len = String.length str in
+    let mem_len = Int32.(to_int (i32 m.size) * to_int (i32 page_size)) in
+    let src = Int32.to_int @@ i32 src in
+    let dst = Int32.to_int @@ i32 dst in
+    let len = Int32.to_int @@ i32 len in
+    if
+      src < 0 || dst < 0 || len < 0
+      || src + len > str_len
+      || dst + len > mem_len
+    then Symbolic_value.Bool.const true
+    else begin
+      for i = 0 to len - 1 do
+        let byte = Char.code @@ String.get str (src + i) in
+        let a = Backend.address_i32 (Int32.of_int (dst + i)) in
+        Backend.storen m.data a (Smtml.Expr.value (Num (I8 byte))) 1
+      done;
+      Symbolic_value.Bool.const false
+    end
+
+  let clone m = { data = Backend.clone m.data; size = m.size }
+
+  let must_be_valid_address m a =
+    let open Symbolic_choice_without_memory in
+    let* addr = Backend.validate_address m a in
+    match addr with Error t -> trap t | Ok ptr -> Backend.address ptr
+
+  let load_8_s m a =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data a in
+    let v = Backend.loadn m.data a 1 in
+    match Smtml.Expr.view v with
+    | Val (Num (I8 i8)) ->
+      Symbolic_value.const_i32 (Int32.extend_s 8 (Int32.of_int i8))
+    | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Sign_extend 24) v
+
+  let load_8_u m a =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data a in
+    let v = Backend.loadn m.data a 1 in
+    match Smtml.Expr.view v with
+    | Val (Num (I8 i)) -> Symbolic_value.const_i32 (Int32.of_int i)
+    | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Zero_extend 24) v
+
+  let load_16_s m a =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data a in
+    let v = Backend.loadn m.data a 2 in
+    match Smtml.Expr.view v with
+    | Val (Num (I32 i16)) -> Symbolic_value.const_i32 (Int32.extend_s 16 i16)
+    | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Sign_extend 16) v
+
+  let load_16_u m a =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data a in
+    let v = Backend.loadn m.data a 2 in
+    match Smtml.Expr.view v with
+    | Val (Num (I32 _)) -> v
+    | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Zero_extend 16) v
+
+  let load_32 m a =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data a in
+    Backend.loadn m.data a 4
+
+  let load_64 m a =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data a in
+    Backend.loadn m.data a 8
+
+  let store_8 m ~addr v =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data addr in
+    Backend.storen m.data a v 1
+
+  let store_16 m ~addr v =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data addr in
+    Backend.storen m.data a v 2
+
+  let store_32 m ~addr v =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data addr in
+    Backend.storen m.data a v 4
+
+  let store_64 m ~addr v =
+    let open Symbolic_choice_without_memory in
+    let+ a = must_be_valid_address m.data addr in
+    Backend.storen m.data a v 8
+
+  let get_limit_max _m = None (* TODO *)
+
+  let free m base = Backend.free m.data base
+
+  let realloc m ~ptr ~size = Backend.realloc m.data ~ptr ~size
+
+  (* TODO: Move this into a separate module? *)
+  module ITbl = Hashtbl.Make (struct
+    include Int
+
+    let hash x = x
+  end)
+
+  type collection = t ITbl.t Env_id.Tbl.t
+
+  let init () = Env_id.Tbl.create 0
+
+  let iter f collection = Env_id.Tbl.iter (fun _ tbl -> f tbl) collection
+
+  let clone collection =
+    (* TODO: this is ugly and should be rewritten *)
+    let s = Env_id.Tbl.to_seq collection in
+    Env_id.Tbl.of_seq
+    @@ Seq.map
+         (fun (i, t) ->
+           let s = ITbl.to_seq t in
+           (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone a)) s) )
+         s
+
+  let convert (orig_mem : Concrete_memory.t) : t =
+    let s = Concrete_memory.size_in_pages orig_mem in
+    create s
+
+  let get_env env_id memories =
+    match Env_id.Tbl.find_opt memories env_id with
+    | Some env -> env
+    | None ->
+      let t = ITbl.create 0 in
+      Env_id.Tbl.add memories env_id t;
+      t
+
+  let get_memory env_id (orig_memory : Concrete_memory.t) collection g_id =
+    let env = get_env env_id collection in
+    match ITbl.find_opt env g_id with
+    | Some t -> t
+    | None ->
+      let t = convert orig_memory in
+      ITbl.add env g_id t;
+      t
+end
diff --git a/src/symbolic/symbolic_memory_make.mli b/src/symbolic/symbolic_memory_make.mli
new file mode 100644
index 000000000..a192b8f61
--- /dev/null
+++ b/src/symbolic/symbolic_memory_make.mli
@@ -0,0 +1,6 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+(** @inline *)
+include Symbolic_memory_intf.Intf
diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml
index 030156750..3999eb902 100644
--- a/src/symbolic/symbolic_wasm_ffi.ml
+++ b/src/symbolic/symbolic_wasm_ffi.ml
@@ -4,7 +4,7 @@
 
 module Expr = Smtml.Expr
 module Choice = Symbolic_choice_with_memory
-module Memory = Symbolic_memory
+module Memory = Symbolic.P.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 *)
 module M :
@@ -43,34 +43,13 @@ module M :
 
   let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol
 
-  open Expr
-
   let abort () : unit Choice.t = Choice.add_pc @@ Value.Bool.const false
 
-  let i32 v : int32 Choice.t =
-    match view v with
-    | Val (Num (I32 v)) -> Choice.return v
-    | _ ->
-      Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v;
-      Choice.bind (abort ()) (fun () -> assert false)
-
-  let ptr v : int32 Choice.t =
-    match view v with
-    | Ptr { base; _ } -> Choice.return base
-    | _ ->
-      Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v;
-      Choice.bind (abort ()) (fun () -> assert false)
-
   let alloc m (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
-    let open Choice in
-    let+ base = i32 base in
-    Memory.replace_size m base size;
-    Expr.ptr base (Value.const_i32 0l)
-
-  let free m (p : Value.int32) : unit Choice.t =
-    let open Choice in
-    let+ base = ptr p in
-    Memory.free m base
+    Choice.lift_mem @@ Memory.realloc m ~ptr:base ~size
+
+  let free m (ptr : Value.int32) : unit Choice.t =
+    Choice.lift_mem @@ Memory.free m ptr
 
   let exit (_p : Value.int32) : unit Choice.t = abort ()
 end
diff --git a/src/symbolic/thread_with_memory.ml b/src/symbolic/thread_with_memory.ml
index 86646e600..887c476f7 100644
--- a/src/symbolic/thread_with_memory.ml
+++ b/src/symbolic/thread_with_memory.ml
@@ -2,7 +2,7 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-include Thread.Make (Symbolic_memory)
+include Thread.Make (Symbolic_memory_concretizing)
 
 let project (th : t) : Thread_without_memory.t * _ =
   let projected =
@@ -24,7 +24,8 @@ let restore backup th =
   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
+    if Thread_without_memory.memories th then
+      Symbolic_memory_concretizing.clone backup
     else backup
   in
   let tables = Thread_without_memory.tables th in
diff --git a/src/symbolic/thread_with_memory.mli b/src/symbolic/thread_with_memory.mli
index 0e93de7a9..7a3f88649 100644
--- a/src/symbolic/thread_with_memory.mli
+++ b/src/symbolic/thread_with_memory.mli
@@ -3,7 +3,8 @@
 (* Written by the Owi programmers *)
 
 (** @inline *)
-include Thread.S with type Memory.collection = Symbolic_memory.collection
+include
+  Thread.S with type Memory.collection = Symbolic_memory_concretizing.collection
 
 val project : t -> Thread_without_memory.t * Memory.collection