Add lift_mem to complete choice monad

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

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

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)