diff --git a/src/colis.ml b/src/colis.ml
index 65bd1857..a15bdf23 100644
--- a/src/colis.ml
+++ b/src/colis.ml
@@ -120,7 +120,7 @@ module Constraints = Colis_constraints
 let () =
   (* Register the utilities to the mixed backend, which is used in interpreting the
      interfaces for constraints and transducers equally *)
-  List.iter SymbolicUtility.Mixed.register [
+  List.iter SymbolicUtility.Mixed.Interpreter.register [
     (module Basics.True) ;
     (module Basics.Colon) ;
     (module Basics.False) ;
@@ -173,13 +173,13 @@ type sym_config = {
 
 module SymbolicConstraints = struct
 
-  type state = SymbolicUtility.Constraints.state
-  type sym_state = SymbolicUtility.Constraints.sym_state
+  type state = SymbolicUtility.Constraints.Interpreter.state
+  type sym_state = SymbolicUtility.Constraints.Interpreter.sym_state
   type config = SymbolicUtility.Constraints.config = {
     prune_init_state: bool;
   }
 
-  let is_registered = SymbolicUtility.Mixed.is_registered
+  let is_registered = SymbolicUtility.Mixed.Interpreter.is_registered
 
   let interp_program ~loop_limit ~stack_size ~argument0 stas' program =
     let open Common in
@@ -210,10 +210,10 @@ module SymbolicConstraints = struct
         fprintf fmt "id: %s@\n" id;
         if !Colis_internals.Options.print_states_dir <> "" then
           let filename = sprintf "%s/%s.dot" !Colis_internals.Options.print_states_dir id in
-          print_dot filename id sta.Constraints.filesystem.clause;
+          print_dot filename id sta.Constraints.Interpreter.filesystem.clause;
       | None -> ()
     end;
-    print_filesystem fmt sta.Constraints.filesystem;
+    print_filesystem fmt sta.Constraints.Interpreter.filesystem;
     (* Print stdin *)
     if sta.stdin <> [] then begin
       fprintf fmt "stdin: |@\n";
@@ -266,8 +266,8 @@ module SymbolicConstraints = struct
     let open SymbolicUtility in
     let context = mk_context ~arguments ~vars in
     let filesystems = Constraints.filesystems config sym_config.filesystem_spec in
-    let stas = List.map Constraints.mk_state filesystems in
-    let sym_stas = List.map (fun state -> Constraints.{ state; context }) stas in
+    let stas = List.map Constraints.Interpreter.mk_state filesystems in
+    let sym_stas = List.map (fun state -> Constraints.Interpreter.{ state; context }) stas in
     let results =
       interp_program ~loop_limit:sym_config.loop_limit ~stack_size:sym_config.stack_size ~argument0
         sym_stas colis
@@ -286,10 +286,10 @@ module SymbolicConstraints = struct
     let root0 = if prune_init_state then None else Some root in
     let filesystem =
       {root; clause; root0} in
-    mk_state filesystem
+    Interpreter.mk_state filesystem
 
   let to_symbolic_state ~vars ~arguments state =
-    SymbolicUtility.Constraints.{state; context = mk_context ~arguments ~vars}
+    SymbolicUtility.Constraints.Interpreter.{state; context = mk_context ~arguments ~vars}
 end
 
 module SymbolicTransducers = struct
@@ -305,8 +305,8 @@ module SymbolicTransducers = struct
         let context = mk_context ~arguments ~vars in
         let stas =
           let fs = Transducers.filesystems config sym_config.filesystem_spec in
-          List.map Transducers.mk_state fs in
-        List.map (fun state -> Transducers.{ state; context }) stas in
+          List.map Transducers.Interpreter.mk_state fs in
+        List.map (fun state -> Transducers.Interpreter.{ state; context }) stas in
       let results = SymbolicUtility.Mixed.interp_program_transducers inp sym_stas colis in
       exit (exit_code results)
 end
diff --git a/src/colis.mli b/src/colis.mli
index 2fe4ddd5..2c6b80cc 100644
--- a/src/colis.mli
+++ b/src/colis.mli
@@ -110,8 +110,8 @@ type sym_config = {
 module SymbolicConstraints : sig
   open Constraints
 
-  type state = SymbolicUtility.Constraints.state
-  type sym_state = SymbolicUtility.Constraints.sym_state
+  type state = SymbolicUtility.Constraints.Interpreter.state
+  type sym_state = SymbolicUtility.Constraints.Interpreter.sym_state
   type config = SymbolicUtility.Constraints.config = {
     prune_init_state: bool; (** Prune the initial symbolic state during symbolic execution for a faster execution *)
   }
diff --git a/src/symbolic/symbolicUtility.ml b/src/symbolic/symbolicUtility.ml
index 8e4df040..338c89c6 100644
--- a/src/symbolic/symbolicUtility.ml
+++ b/src/symbolic/symbolicUtility.ml
@@ -33,6 +33,12 @@ module type INTERPRETER = sig
   val incomplete : utility:string -> string -> utility
   val unknown : utility:string -> string -> utility
 
+  type utility_context = Semantics__UtilityContext.utility_context = {
+    cwd: Colis_constraints.Path.normal;
+    env: string Env.SMap.t;
+    args: string list;
+  }
+
   module type SYMBOLIC_UTILITY = sig
     val name : string
     val interprete : utility_context -> utility
@@ -421,10 +427,8 @@ module Concrete = struct
     let apply_spec fs spec = Option.to_list (spec fs)
   end
   module Interpreter = MakeInterpreter (Filesystem)
-  include MakeCombinators (Interpreter)
-  include MakeSpecifications (Interpreter) (CaseSpec)
-  include Filesystem
-  include Interpreter
+  module Combinators = MakeCombinators (Interpreter)
+  module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
   include CaseSpec
 
   type config = unit
@@ -473,10 +477,8 @@ module Constraints = struct
   end
 
   module Interpreter = MakeInterpreter (Filesystem)
-  include MakeCombinators (Interpreter)
-  include MakeSpecifications (Interpreter) (CaseSpec)
-  include Filesystem
-  include Interpreter
+  module Combinators = MakeCombinators (Interpreter)
+  module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
   include CaseSpec
 
   type config = { prune_init_state : bool }
@@ -506,10 +508,8 @@ module Transducers = struct
   end
 
   module Interpreter = MakeInterpreter (Filesystem)
-  include MakeCombinators (Interpreter)
-  include MakeSpecifications (Interpreter) (CaseSpec)
-  include Filesystem
-  include Interpreter
+  module Combinators = MakeCombinators (Interpreter)
+  module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
   include CaseSpec
 
   type config = unit
@@ -567,27 +567,25 @@ module Mixed = struct
   end
 
   module Interpreter = MakeInterpreter (Filesystem)
-  include MakeCombinators (Interpreter)
-  include MakeSpecifications (Interpreter) (CaseSpec)
-  include Filesystem
-  include Interpreter
+  module Combinators = MakeCombinators (Interpreter)
+  module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
   include CaseSpec
 
   (* Concrete interpretation *)
 
-  let state_from_concrete (s : Concrete.state) : state = {
+  let state_from_concrete (s : Concrete.Interpreter.state) : Interpreter.state = {
     filesystem=Concrete s.filesystem;
     stdin=s.stdin;
     stdout=s.stdout;
     log=s.log;
   }
 
-  let sym_state_from_concrete (s: Concrete.sym_state) : sym_state = {
+  let sym_state_from_concrete (s: Concrete.Interpreter.sym_state) : Interpreter.sym_state = {
     state = state_from_concrete s.state;
     context = s.context;
   }
 
-  let state_to_concrete (s: state) : Concrete.state =
+  let state_to_concrete (s: Interpreter.state) : Concrete.Interpreter.state =
     let filesystem =
       match s.filesystem with
       | Concrete fs -> fs
@@ -596,26 +594,26 @@ module Mixed = struct
 
   let interp_program_concrete inp stas pro =
     let stas' = List.map sym_state_from_concrete stas in
-    let normals, errors, failures = interp_program inp stas' pro in
+    let normals, errors, failures = Interpreter.interp_program inp stas' pro in
     List.map state_to_concrete normals,
     List.map state_to_concrete errors,
     List.map state_to_concrete failures
 
   (* Constraints interpretation *)
 
-  let state_from_constraints (s : Constraints.state) : state = {
+  let state_from_constraints (s : Constraints.Interpreter.state) : Interpreter.state = {
     filesystem=Constraints s.filesystem;
     stdin=s.stdin;
     stdout=s.stdout;
     log=s.log;
   }
 
-  let sym_state_from_constraints (s: Constraints.sym_state) : sym_state = {
+  let sym_state_from_constraints (s: Constraints.Interpreter.sym_state) : Interpreter.sym_state = {
     state = state_from_constraints s.state;
     context = s.context;
   }
 
-  let state_to_constraints (s: state) : Constraints.state =
+  let state_to_constraints (s: Interpreter.state) : Constraints.Interpreter.state =
     let filesystem =
       match s.filesystem with
       | Constraints fs -> fs
@@ -624,26 +622,26 @@ module Mixed = struct
 
   let interp_program_constraints inp stas pro =
     let stas' = List.map sym_state_from_constraints stas in
-    let normals, errors, failures = interp_program inp stas' pro in
+    let normals, errors, failures = Interpreter.interp_program inp stas' pro in
     List.map state_to_constraints normals,
     List.map state_to_constraints errors,
     List.map state_to_constraints failures
 
   (* Transducers interpretation *)
 
-  let state_from_transducers (s : Transducers.state) : state = {
+  let state_from_transducers (s : Transducers.Interpreter.state) : Interpreter.state = {
     filesystem=Transducers s.filesystem;
     stdin=s.stdin;
     stdout=s.stdout;
     log=s.log;
   }
 
-  let sym_state_from_transducers (s: Transducers.sym_state) : sym_state = {
+  let sym_state_from_transducers (s: Transducers.Interpreter.sym_state) : Interpreter.sym_state = {
     state = state_from_transducers s.state;
     context = s.context;
   }
 
-  let state_to_transducers (s: state) : Transducers.state =
+  let state_to_transducers (s: Interpreter.state) : Transducers.Interpreter.state =
     let filesystem =
       match s.filesystem with
       | Transducers fs -> fs
@@ -652,7 +650,7 @@ module Mixed = struct
 
   let interp_program_transducers inp stas pro =
     let stas' = List.map sym_state_from_transducers stas in
-    let normals, errors, failures = interp_program inp stas' pro in
+    let normals, errors, failures = Interpreter.interp_program inp stas' pro in
     List.map state_to_transducers normals,
     List.map state_to_transducers errors,
     List.map state_to_transducers failures
@@ -660,16 +658,18 @@ end
 
 module ConstraintsCompatibility = struct
 
-  include Mixed
+  include Mixed.Interpreter
+  include Mixed.Specifications
+  include Mixed.Combinators
 
   let success_case ~descr ?stdout constraints =
-    success_case ~descr ?stdout (case_spec ~constraints ())
+    success_case ~descr ?stdout (Mixed.case_spec ~constraints ())
 
   let error_case ~descr ?stdout ?error_message constraints =
-    error_case ~descr ?stdout ?error_message (case_spec ~constraints ())
+    error_case ~descr ?stdout ?error_message (Mixed.case_spec ~constraints ())
 
   let incomplete_case ~descr constraints =
-    incomplete_case ~descr (case_spec ~constraints ())
+    incomplete_case ~descr (Mixed.case_spec ~constraints ())
 
   let noop = Constraints.noop
 end
diff --git a/src/symbolic/symbolicUtility.mli b/src/symbolic/symbolicUtility.mli
index d27a2ec1..234d8c71 100644
--- a/src/symbolic/symbolicUtility.mli
+++ b/src/symbolic/symbolicUtility.mli
@@ -73,6 +73,13 @@ module type INTERPRETER = sig
 
   (** {4 Registration and dispatch} *)
 
+  (** Alias for easier access in the utility implementations. *)
+  type utility_context = Semantics__UtilityContext.utility_context = {
+    cwd: Colis_constraints.Path.normal;
+    env: string Env.SMap.t;
+    args: string list;
+  }
+
   (** A symbolic utility is comprised of a name and a function that interpretes a [utility]
       in a [context]. *)
   module type SYMBOLIC_UTILITY = sig
@@ -212,10 +219,32 @@ module MakeSpecifications
 
 (** {1 Backends} *)
 
+(** {2 Concrete backend}
+
+    Incomplete - just a simplest possible showcase. *)
+
+module Concrete : sig
+  type filesystem = FilesystemSpec.t
+  type case_spec = filesystem -> filesystem option
+
+  module Interpreter : INTERPRETER
+    with type filesystem := filesystem
+
+  module Combinators : COMBINATORS
+    with type state := Interpreter.state
+
+  module Specifications : SPECIFICATIONS
+    with type state := Interpreter.state
+     and type case_spec := filesystem -> filesystem option
+
+  type config = unit
+  val filesystems : config -> FilesystemSpec.t -> filesystem list
+end
+
 (** {2 Constraints} *)
 
 (** Instantiation of the constraints-based backend with the interpreter and
-   specifications. *)
+    specifications. *)
 module Constraints : sig
 
   open Colis_constraints
@@ -233,14 +262,14 @@ module Constraints : sig
      the new root [r] to a constraint clause [c]. *)
   type case_spec = Var.t -> Var.t -> Clause.t
 
-  include INTERPRETER
+  module Interpreter : INTERPRETER
     with type filesystem := filesystem
 
-  include COMBINATORS
-    with type state := state
+  module Combinators : COMBINATORS
+    with type state := Interpreter.state
 
-  include SPECIFICATIONS
-    with type state := state
+  module Specifications : SPECIFICATIONS
+    with type state := Interpreter.state
      and type case_spec := case_spec
 
   type config = {
@@ -261,41 +290,20 @@ module Transducers : sig
   type filesystem = unit
   type case_spec = unit
 
-  include INTERPRETER
-    with type filesystem := filesystem
-
-  include COMBINATORS
-    with type state := state
-
-  include SPECIFICATIONS
-    with type state := state
-     and type case_spec := case_spec
-
-  type config = unit
-  val filesystems : config -> FilesystemSpec.t -> filesystem list
-end
-
-(** {2 Concrete backend}*)
-
-module Concrete : sig
-  type filesystem = FilesystemSpec.t
-  type case_spec = filesystem -> filesystem option
-
-  include INTERPRETER
+  module Interpreter : INTERPRETER
     with type filesystem := filesystem
 
-  include COMBINATORS
-    with type state := state
+  module Combinators : COMBINATORS
+    with type state := Interpreter.state
 
-  include SPECIFICATIONS
-    with type state := state
+  module Specifications : SPECIFICATIONS
+    with type state := Interpreter.state
      and type case_spec := case_spec
 
   type config = unit
   val filesystems : config -> FilesystemSpec.t -> filesystem list
 end
 
-
 (** {2 Mixed constraints/transducers}
 
     The mixed backend combines the constraints-based backend with the transducers-based
@@ -314,34 +322,27 @@ module Mixed : sig
     ?constraints:Constraints.case_spec ->
     unit -> case_spec
 
-  include INTERPRETER
+  module Interpreter : INTERPRETER
     with type filesystem := filesystem
 
-  include COMBINATORS
-    with type state := state
+  module Combinators : COMBINATORS
+    with type state := Interpreter.state
 
-  include SPECIFICATIONS
-    with type state := state
+  module Specifications : SPECIFICATIONS
+    with type state := Interpreter.state
      and type case_spec := case_spec
 
   (** Symbolically interprete a program using the constraints backend *)
-  val interp_program_constraints : input -> Constraints.sym_state list -> program ->
-    (Constraints.state list * Constraints.state list * Constraints.state list)
-
-  (** Symbolically interprete a program using the transducers backend *)
-  val interp_program_transducers : input -> Transducers.sym_state list -> program ->
-    (Transducers.state list * Transducers.state list * Transducers.state list)
+  val interp_program_concrete : input -> Concrete.Interpreter.sym_state list -> program ->
+    Concrete.Interpreter.state list * Concrete.Interpreter.state list * Concrete.Interpreter.state list
 
   (** Symbolically interprete a program using the constraints backend *)
-  val interp_program_concrete : input -> Concrete.sym_state list -> program ->
-    (Concrete.state list * Concrete.state list * Concrete.state list)
+  val interp_program_constraints : input -> Constraints.Interpreter.sym_state list -> program ->
+    Constraints.Interpreter.state list * Constraints.Interpreter.state list * Constraints.Interpreter.state list
 
-  (** Alias for easier access in the utility implementations. *)
-  type utility_context = Semantics__UtilityContext.utility_context = {
-    cwd: Colis_constraints.Path.normal;
-    env: string Env.SMap.t;
-    args: string list;
-  }
+  (** Symbolically interprete a program using the transducers backend *)
+  val interp_program_transducers : input -> Transducers.Interpreter.sym_state list -> program ->
+    Transducers.Interpreter.state list * Transducers.Interpreter.state list * Transducers.Interpreter.state list
 end
 
 (** {2 Compatibility}
@@ -349,12 +350,21 @@ end
     Compatibility with module SymbolicUtility before functorization of the symbolic
    engine: Create mixed utilities with the interface of constraints-based backend. *)
 module ConstraintsCompatibility : sig
-  include module type of Mixed
+
+  include INTERPRETER
     with type filesystem = Mixed.filesystem
-     and type state = Mixed.state
+     and type state := Mixed.Interpreter.state
+
+  include COMBINATORS
+    with type state := Mixed.Interpreter.state
+
+  include SPECIFICATIONS
+    with type state := Mixed.Interpreter.state
+     and type case_spec = Mixed.case_spec
+     and type case := Mixed.Specifications.case
 
-  val success_case: descr:string -> ?stdout:Stdout.t -> Constraints.case_spec -> case
-  val error_case: descr:string -> ?stdout:Stdout.t -> ?error_message:string -> Constraints.case_spec -> case
-  val incomplete_case: descr:string -> Constraints.case_spec -> case
+  val success_case: descr:string -> ?stdout:Stdout.t -> Constraints.case_spec -> Mixed.Specifications.case
+  val error_case: descr:string -> ?stdout:Stdout.t -> ?error_message:string -> Constraints.case_spec -> Mixed.Specifications.case
+  val incomplete_case: descr:string -> Constraints.case_spec -> Mixed.Specifications.case
   val noop : Constraints.case_spec
 end
diff --git a/src/symbolic/utilities/mkdir.ml b/src/symbolic/utilities/mkdir.ml
index fa88a463..783bfae0 100644
--- a/src/symbolic/utilities/mkdir.ml
+++ b/src/symbolic/utilities/mkdir.ml
@@ -2,6 +2,7 @@ open Format
 open Colis_constraints
 open Clause
 open SymbolicUtility.Mixed
+open SymbolicUtility.Mixed.Specifications
 
 let name = "mkdir"
 
@@ -62,12 +63,12 @@ let interp_mkdir1 cwd path_str =
     ]
 
 let interprete parents ctx args : utility =
-  if parents then incomplete ~utility:name "option -p" else
-  multiple_times (interp_mkdir1 ctx.cwd) args
+  if parents then Interpreter.incomplete ~utility:name "option -p" else
+  Combinators.multiple_times (interp_mkdir1 ctx.Interpreter.cwd) args
 
 let interprete ctx : utility =
   let parents = Cmdliner.Arg.(value & flag & info ["p"; "parents"]) in
-  cmdliner_eval_utility
+  Combinators.cmdliner_eval_utility
     ~utility:name
     Cmdliner.Term.(const interprete $ parents)
     ctx
diff --git a/src/symbolic/utilities/mkdir.mli b/src/symbolic/utilities/mkdir.mli
index 427a4a8b..99572e1b 100644
--- a/src/symbolic/utilities/mkdir.mli
+++ b/src/symbolic/utilities/mkdir.mli
@@ -1,5 +1,5 @@
 (** Symbolic execution of mkdir *)
-open SymbolicUtility.Mixed
+open SymbolicUtility.Mixed.Interpreter
 
 val name : string
 val interprete : utility_context -> utility