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/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml
index c0f612d0c..5dd8249b8 100644
--- a/src/symbolic/symbolic_choice.ml
+++ b/src/symbolic/symbolic_choice.ml
@@ -225,9 +225,10 @@ module CoreImpl = struct
       other =
       St
         (fun st ->
+          let ( let* ) = M.( let* ) in
           let proj, backup = project_and_backup st in
-          M.bind (run other proj) (fun (res, new_state) ->
-              M.return (res, restore backup new_state) ) )
+          let* res, new_state = run other proj in
+          M.return (res, restore backup new_state) )
   end
 
   module Eval = struct
diff --git a/src/symbolic/symbolic_choice_minimalist.ml b/src/symbolic/symbolic_choice_minimalist.ml
index 8857cddf7..9dcddac6e 100644
--- a/src/symbolic/symbolic_choice_minimalist.ml
+++ b/src/symbolic/symbolic_choice_minimalist.ml
@@ -66,6 +66,8 @@ module Make (Thread : Thread.S) = struct
   let add_pc (_vb : vbool) = return ()
 
   let run ~workers:_ solver t thread = run t thread (Solver.fresh solver ())
+
+  let lift_mem _ = assert false
 end
 
 include Make (Thread_with_memory)