diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml
index 33e6a9ed9..d9d15cc89 100644
--- a/src/cmd/cmd_sym.ml
+++ b/src/cmd/cmd_sym.ml
@@ -109,7 +109,6 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
     else results
   in
   let* count = print_and_count_failures 0 results in
-  Format.pp_std "completed paths: %d@." !path_counter;
   if count > 0 then Error (`Found_bug count)
   else begin
     Fmt.pr "All OK";
diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml
index 5dd8249b8..366b3a77f 100644
--- a/src/symbolic/symbolic_choice.ml
+++ b/src/symbolic/symbolic_choice.ml
@@ -225,10 +225,10 @@ module CoreImpl = struct
       other =
       St
         (fun st ->
-          let ( let* ) = M.( let* ) in
+          let ( let+ ) = M.( let+ ) in
           let proj, backup = project_and_backup st in
-          let* res, new_state = run other proj in
-          M.return (res, restore backup new_state) )
+          let+ res, new_state = run other proj in
+          (res, restore backup new_state) )
   end
 
   module Eval = struct
@@ -274,7 +274,9 @@ module CoreImpl = struct
   end
 
   (*  *)
-  module Make (Thread : Thread.S) = struct
+  module Make (Thread : Thread.S) :
+    S with type thread := Thread.t and type 'a t = ('a, Thread.t) Eval.t =
+  struct
     include Eval
 
     type 'a t = ('a, Thread.t) Eval.t
@@ -343,7 +345,6 @@ end
     We can now use CoreImpl only through its exposed signature which
     maintains all invariants.
   *)
-(* module CoreImpl' : S = CoreImpl *)
 
 module Make (Thread : Thread.S) = struct
   include CoreImpl.Make (Thread)
diff --git a/src/symbolic/symbolic_choice_with_memory.ml b/src/symbolic/symbolic_choice_with_memory.ml
index a15689a8a..d143f5d0b 100644
--- a/src/symbolic/symbolic_choice_with_memory.ml
+++ b/src/symbolic/symbolic_choice_with_memory.ml
@@ -1,3 +1,7 @@
+(* 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 =
diff --git a/src/symbolic/.symbolic_choice.mli b/src/symbolic/symbolic_choice_with_memory.mli
similarity index 78%
rename from src/symbolic/.symbolic_choice.mli
rename to src/symbolic/symbolic_choice_with_memory.mli
index c52a97c0d..602df230b 100644
--- a/src/symbolic/.symbolic_choice.mli
+++ b/src/symbolic/symbolic_choice_with_memory.mli
@@ -9,8 +9,7 @@ type 'a eval = private
 
 include
   Choice_intf.Complete
-    with type thread := Thread.t
-     and type 'a run_result = ('a eval * Thread.t) Seq.t
+    with type thread := Thread_with_memory.t
      and module V := Symbolic_value
 
 val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
@@ -19,8 +18,8 @@ val run :
      workers:int
   -> Smtml.Solver_dispatcher.solver_type
   -> 'a t
-  -> Thread.t
-  -> callback:('a eval * Thread.t -> unit)
+  -> Thread_with_memory.t
+  -> callback:('a eval * Thread_with_memory.t -> unit)
   -> callback_init:(unit -> unit)
   -> callback_end:(unit -> unit)
   -> unit Domain.t array
diff --git a/src/symbolic/symbolic_choice_without_memory.ml b/src/symbolic/symbolic_choice_without_memory.ml
index 4351d9b18..5041426ce 100644
--- a/src/symbolic/symbolic_choice_without_memory.ml
+++ b/src/symbolic/symbolic_choice_without_memory.ml
@@ -1 +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..e44339c9b
--- /dev/null
+++ b/src/symbolic/symbolic_choice_without_memory.mli
@@ -0,0 +1,42 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* 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
+
+type 'a t = ('a, Thread_without_memory.t) Symbolic_choice.CoreImpl.Eval.t
+
+type thread := Thread_without_memory.t
+
+module V := Symbolic_value
+
+type 'a run_result
+
+val return : 'a -> 'a t
+
+val bind : 'a t -> ('a -> 'b t) -> 'b t
+
+val map : 'a t -> ('a -> 'b) -> 'b t
+
+val select : V.vbool -> bool t
+
+val select_i32 : V.int32 -> Int32.t t
+
+val trap : Trap.t -> 'a t
+
+val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+val assertion : V.vbool -> unit t
+
+val with_thread : (thread -> 'b) -> 'b t
+
+val solver : Solver.t t
+
+val thread : thread t
+
+val add_pc : V.vbool -> unit t