diff --git a/src/symbolic/symbolicUtility.ml b/src/symbolic/symbolicUtility.ml
index 94e38f49..23500bba 100644
--- a/src/symbolic/symbolicUtility.ml
+++ b/src/symbolic/symbolicUtility.ml
@@ -97,9 +97,14 @@ let print_utility_trace str sta =
     let log = print_output ~newline:true ("[UTL] "^str) sta.log in
     {sta with log}
 
+type case_spec = Var.t -> Var.t -> Clause.t
+
+let noop : case_spec =
+  Clause.eq
+
 type case = {
   result : bool;
-  spec : Clause.t;
+  spec : case_spec;
   descr : string;
   stdout : Stdout.t ;
   error_message: string option;
@@ -111,24 +116,32 @@ let success_case ~descr ?(stdout=Stdout.empty) spec =
 let error_case ~descr ?(stdout=Stdout.empty) ?error_message spec =
   { result = false ; error_message ; stdout ; descr ; spec }
 
-let failure ?error_message ~root ~root' =
+let failure ~error_message =
   [{ result = false ;
      descr = "" ;
      stdout = Stdout.empty ;
-     error_message ;
-     spec = Clause.eq root root' }]
-
-let quantify_over_intermediate_root fs conj =
-  if BatOption.eq ~eq:Var.equal fs.SymbolicInterpreter__Filesystem.root0 (Some fs.root) then
-    [conj]
-  else
-    Clause.quantify_over_and_simplify fs.root conj
+     error_message = Some error_message;
+     spec = noop }]
+
+let add_spec sta spec : state list =
+  let root' = Var.fresh ~hint:(Var.hint sta.filesystem.root) () in
+  let clause = spec sta.filesystem.root root' in
+  let clauses = Clause.add_to_sat_conj clause sta.filesystem.clause in
+  let clauses =
+    match sta.filesystem.SymbolicInterpreter__Filesystem.root0 with
+    | Some root0 when Var.equal root0 sta.filesystem.SymbolicInterpreter__Filesystem.root ->
+      clauses
+    | _ -> (* root0 is either None or different than Some root: we thus can garbage-collect the current root *)
+      clauses |>
+      List.map (Clause.quantify_over_and_simplify sta.filesystem.SymbolicInterpreter__Filesystem.root) |>
+      List.flatten in
+  List.map (fun clause -> {sta with filesystem={sta.filesystem with clause; root=root'}}) clauses
 
 (** Update a state with a specification case and a new root [root'].
 
     This may result in multiple states because the integration of the case clause in the
     filesystem may result in multiple clauses. *)
-let apply_case_to_state sta root' case : (state * bool) list =
+let apply_case_to_state sta case : (state * bool) list =
   (* First print the utility trace *)
   let sta = print_utility_trace case.descr sta in
   let sta = {
@@ -143,23 +156,16 @@ let apply_case_to_state sta root' case : (state * bool) list =
   (* (Optionally) print error message *)
   let sta = print_error case.error_message sta in
   (* Combine the case specification and the current filesystem clause *)
-  Clause.add_to_sat_conj case.spec sta.filesystem.clause
-  |> List.map (quantify_over_intermediate_root sta.filesystem)
-  |> List.flatten
-  (* ... now update the filesystem in the state with the new clauses and the new root *)
-  |> List.map (fun clause ->
-      let filesystem = {sta.filesystem with clause; root=root'} in
-      {sta with filesystem})
-  (* and combine each state with the case result *)
-  |> List.map (fun sta -> sta, case.result)
-
-type specifications = root:Var.t -> root':Var.t -> case list
+  let stas = add_spec sta case.spec in
+  (* Add the result to each result state *)
+  List.map (fun sta -> sta, case.result) stas
+
+type specifications = case list
 
 let under_specifications : specifications -> state -> (state * bool) list =
   fun spec state ->
-    let new_root = Var.fresh ~hint:(Var.hint state.filesystem.root) () in
-    let cases = spec ~root:state.filesystem.root ~root':new_root in
-    List.map (apply_case_to_state state new_root) cases |> List.flatten
+  List.flatten
+    (List.map (apply_case_to_state state) spec)
 
 (******************************************************************************)
 (*                                  Auxiliaries                               *)
diff --git a/src/symbolic/symbolicUtility.mli b/src/symbolic/symbolicUtility.mli
index 9e510513..dcf6bcb5 100644
--- a/src/symbolic/symbolicUtility.mli
+++ b/src/symbolic/symbolicUtility.mli
@@ -28,22 +28,26 @@ end
 (** A case in the specification is either a success or an error *)
 type case
 
+(** A case specification is a function from the old root variable and the new root root
+    variable to a clause. *)
+type case_spec = Var.t -> Var.t -> Clause.t
+
+(** The no-op case specification introduces an equality constraint between the old root
+    and the new root. *)
+val noop : case_spec
+
 (** A success case *)
-val success_case: descr:string -> ?stdout:Stdout.t -> Clause.t -> case
+val success_case: descr:string -> ?stdout:Stdout.t -> case_spec -> case
 
 (** An error case *)
-val error_case: descr:string -> ?stdout:Stdout.t -> ?error_message:string -> Clause.t -> case
+val error_case: descr:string -> ?stdout:Stdout.t -> ?error_message:string -> case_spec -> case
+
+(** A singleton error case with optional error message *)
+val failure: error_message:string -> case list
 
 (** The specifications of a utility are a list of cases that depend on the current working
     directory, the old root variable, and a new root variable *)
-type specifications = root:Var.t -> root':Var.t -> case list
-
-(* TODO Move root, root' arguments from [specifications] to clause argument of cases.
-   That's where they belong and it would allow the definition of [val identity : Var.t ->
-   Var.t -> Clause.t], which isn't currently possible. *)
-
-(** A singleton error case with optional error message *)
-val failure: ?error_message:string -> root:Var.t -> root':Var.t -> case list
+type specifications = case list
 
 (** Use specifications to define a utility *)
 val under_specifications : specifications -> utility
diff --git a/src/symbolic/utilities/colisInternalUnsafeTouch.ml b/src/symbolic/utilities/colisInternalUnsafeTouch.ml
index 44c54e0c..0b2a8287 100644
--- a/src/symbolic/utilities/colisInternalUnsafeTouch.ml
+++ b/src/symbolic/utilities/colisInternalUnsafeTouch.ml
@@ -6,13 +6,12 @@ open SymbolicUtility
 let name = "colis_internal_unsafe_touch"
 
 let interp1 path_str =
-  under_specifications @@ fun ~root ~root' ->
   let p = Path.from_string path_str in
   let q = Path.check_normal p in
-  [
+  under_specifications [
     success_case
       ~descr:(asprintf "colis_internal_unsafe_touch: %a" Path.pp p)
-      begin
+      begin fun root root' ->
         (* FIXME: one could do better and drop the last maybe on the left. *)
         let rec aux x x' = function
           | [] ->
diff --git a/src/symbolic/cp.ml b/src/symbolic/utilities/cp.ml
similarity index 83%
rename from src/symbolic/cp.ml
rename to src/symbolic/utilities/cp.ml
index 48df9343..8cccfb88 100644
--- a/src/symbolic/cp.ml
+++ b/src/symbolic/utilities/cp.ml
@@ -10,33 +10,30 @@ let name = "cp"
  * Recursive copy if isrec.
  *)
 let interp_cp2 ctx ~todir ~isrec src dst : utility =
-  under_specifications @@ fun ~root ~root' ->
   let qsrc = Path.from_string src in
   let qdst = Path.from_string dst in
+  under_specifications @@
   match Path.split_last qsrc, Path.split_last qdst with
   | (None, _) ->
-     failure ~error_message:"cp: invalid source path ''" ~root ~root'
+     failure ~error_message:"cp: invalid source path ''"
   | (_, None) ->
-     failure ~error_message:"cp: invalid destination path ''" ~root ~root'
+     failure ~error_message:"cp: invalid destination path ''"
   | (Some (_, (Here|Up)), _) ->
      (* TODO: "For each source_file, the following steps ...
         source file is dot or dot-dot, cp should do nothing
         with source file and go to any remaining file" *)
-     failure ~error_message:"cp: source path ends in . or .." ~root ~root'
+     failure ~error_message:"cp: source path ends in . or .."
   | (_, Some (_, (Here|Up))) -> (* Unreachable or error path *)
-     failure ~error_message:"cp: destination path ends in . or .." ~root ~root'
+     failure ~error_message:"cp: destination path ends in . or .."
   | (Some (_qs, Down fs), Some (qd, efd)) ->
      let stripdst = Path.strip_trailing_slashes dst in
      let newdst = String.concat "/" [stripdst; (Feat.to_string fs)] in
      let dstpath = Path.from_string newdst in
-
-     let hintys = last_comp_as_hint ~root qsrc in
-     let hintxd = last_comp_as_hint ~root qd in
-     let hintyd = last_comp_as_hint ~root qdst in
-     let src_no_file_cases = [
+     let src_no_file_cases =
+       [
          error_case
            ~descr:(asprintf "cp: no such file source '%s'" src)
-           begin
+           begin fun root root' ->
              noresolve root ctx.cwd qsrc
              & eq root root'
            end
@@ -45,14 +42,16 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
          else [
            error_case
            ~descr:(asprintf "cp: source '%s' is a directory, option '-R' required" src)
-           begin
+           begin fun root root' ->
+             let hintys = last_comp_as_hint ~root qsrc in
              exists ?hint:hintys @@ fun ys ->
              resolve root ctx.cwd qsrc ys & dir ys
              & eq root root'
            end;
            error_case
            ~descr:(asprintf "cp: '%a' is a directory, option '-R' required" Path.pp dstpath)
-           begin
+           begin fun root root' ->
+             let hintys = last_comp_as_hint ~root qsrc in
              exists2 ?hint1:hintys ?hint2:None @@ fun ys zd ->
              resolve root ctx.cwd qsrc ys & ndir ys
              & resolve root ctx.cwd dstpath zd & dir zd
@@ -64,13 +63,14 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
      let dst_no_path_cases = [
         error_case
           ~descr:(asprintf "cp: no such file '%a'" Path.pp qd)
-          begin
+          begin fun root root' ->
             noresolve root ctx.cwd qd
             & eq root root'
           end;
         error_case
           ~descr:(asprintf "cp: not a directory '%a'" Path.pp qd)
-          begin
+          begin fun root root' ->
+            let hintxd = last_comp_as_hint ~root qd in
             exists ?hint:hintxd @@ fun xd ->
             resolve root ctx.cwd qd xd & ndir xd
             & eq root root'
@@ -83,14 +83,16 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
           [
            error_case
              ~descr:(asprintf "cp: destination directory '%s' does not exist" dst)
-            begin
+            begin fun root root' ->
               noresolve root ctx.cwd qdst & eq root root'
             end
          ]
        | true, false, Down fd -> [
            success_case
              ~descr:(asprintf "cp: source dir '%s' in new dir '%s'" src dst)
-             begin
+             begin fun root root' ->
+               let hintys = last_comp_as_hint ~root qsrc in
+               let hintxd = last_comp_as_hint ~root qd in
                exists3 ?hint1:hintys ?hint2:hintxd ?hint3:None @@ fun ys xd xd' ->
                resolve root ctx.cwd qsrc ys & dir ys
                & resolve root ctx.cwd qd xd & abs xd fd
@@ -102,7 +104,8 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
        | false, false, Down fd -> [
            success_case
              ~descr:(asprintf "cp: source file '%s' to new file '%s'" src dst)
-             begin
+             begin fun root root' ->
+               let hintys = last_comp_as_hint ~root qsrc in
                exists ?hint:hintys @@ fun ys ->
                exists2 ?hint1:None ?hint2:None @@ fun xd xd' ->
                resolve root ctx.cwd qsrc ys & ndir ys
@@ -114,7 +117,9 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
              end;
            success_case
              ~descr:(asprintf "cp file '%s' to new file '%s'" src dst)
-             begin
+             begin fun root root' ->
+               let hintys = last_comp_as_hint ~root qsrc in
+               let hintyd = last_comp_as_hint ~root qdst in
                exists2 ?hint1:hintys ?hint2:hintyd @@ fun ys yd ->
                exists2 ?hint1:None ?hint2:None @@ fun xd xd' ->
                resolve root ctx.cwd qsrc ys & ndir ys
@@ -128,7 +133,9 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
        let src_file_cases = [
            success_case
              ~descr:(asprintf "cp: source file '%s' to directory '%s'" src dst)
-           begin
+           begin fun root root' ->
+             let hintys = last_comp_as_hint ~root qsrc in
+             let hintyd = last_comp_as_hint ~root qdst in
              exists ?hint:hintys @@ fun ys ->
              exists2 ?hint1:hintyd ?hint2:None @@ fun yd yd' ->
              resolve root ctx.cwd qsrc ys & ndir ys
@@ -140,7 +147,9 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
            end;
            success_case
            ~descr:(asprintf "cp: source file '%s' to directory '%s'" src dst)
-           begin
+           begin fun root root' ->
+             let hintys = last_comp_as_hint ~root qsrc in
+             let hintyd = last_comp_as_hint ~root qdst in
              exists ?hint:hintys @@ fun ys ->
              exists3 ?hint1:hintyd ?hint2:None ?hint3:None @@ fun yd yd' zd ->
              resolve root ctx.cwd qsrc ys & ndir ys
@@ -156,7 +165,9 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
          else [
              success_case
                ~descr:(asprintf "cp: destination dir '%s' does not exist" dst)
-               begin
+               begin fun root root' ->
+                 let hintys = last_comp_as_hint ~root qsrc in
+                 let hintyd = last_comp_as_hint ~root qdst in
                  exists ?hint:hintys @@ fun ys ->
                  exists2 ?hint1:hintyd ?hint2:None @@ fun yd yd' ->
                  resolve root ctx.cwd qsrc ys & dir ys
@@ -168,7 +179,8 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
                end;
              success_case
                ~descr:(asprintf "cp: empty directory '%a' exists" Path.pp dstpath)
-               begin
+               begin fun root root' ->
+                 let hintys = last_comp_as_hint ~root qsrc in
                  exists2 ?hint1:hintys ?hint2:None @@ fun ys zd ->
                  resolve root ctx.cwd qsrc ys & dir ys
                  & resolve root ctx.cwd dstpath zd & dir zd
@@ -177,7 +189,8 @@ let interp_cp2 ctx ~todir ~isrec src dst : utility =
                end;
              success_case
                ~descr:(asprintf "cp: non empty directory '%a' exists" Path.pp dstpath)
-               begin
+               begin fun root root' ->
+                 let hintys = last_comp_as_hint ~root qsrc in
                  exists ?hint:hintys @@ fun ys ->
                  exists2 ?hint1:None ?hint2:None @@ fun zd zd' ->
                  resolve root ctx.cwd qsrc ys & dir ys
diff --git a/src/symbolic/cp.mli b/src/symbolic/utilities/cp.mli
similarity index 100%
rename from src/symbolic/cp.mli
rename to src/symbolic/utilities/cp.mli
diff --git a/src/symbolic/utilities/emacsPackage.ml b/src/symbolic/utilities/emacsPackage.ml
index 02f87f33..b228753e 100644
--- a/src/symbolic/utilities/emacsPackage.ml
+++ b/src/symbolic/utilities/emacsPackage.ml
@@ -1,6 +1,4 @@
 open Format
-open Colis_constraints
-open Clause
 open SymbolicUtility
 
 module Install = struct
@@ -18,15 +16,11 @@ module Install = struct
       (if_then_else
          (call "test" ctx ["-e"; pkgFile])
          (call "rm" ctx [pkgFile])
-         (under_specifications @@ fun ~root ~root' ->
-          [
+         (under_specifications [
             success_case
               ~descr:(asprintf "emacs-package-install --preinst '%s': not found"
                         pkgFile)
-              begin
-                eq root root'
-              end
-          ;
+              noop
           ]
          )
       )
@@ -58,15 +52,11 @@ module Remove = struct
     (if_then_else
        (call "test" ctx ["-e"; pkgFile])
        (call "rm" ctx [pkgFile])
-       (under_specifications @@ fun ~root ~root' ->
-        [
+       (under_specifications [
           success_case
             ~descr:(asprintf "emacs-package-install --preinst '%s': not found"
                       pkgFile)
-            begin
-              eq root root'
-            end
-        ;
+            noop
         ]
        )
     )
diff --git a/src/symbolic/utilities/mkdir.ml b/src/symbolic/utilities/mkdir.ml
index c1be4302..2ee3a10e 100644
--- a/src/symbolic/utilities/mkdir.ml
+++ b/src/symbolic/utilities/mkdir.ml
@@ -6,19 +6,19 @@ open SymbolicUtility
 let name = "mkdir"
 
 let interp_mkdir1 cwd path_str =
-  under_specifications @@ fun ~root ~root' ->
   let p = Path.from_string path_str in
+  under_specifications @@
   match Path.split_last p with
   | None ->
-    failure ~error_message:"mkdir: cannot create directory ''" ~root ~root'
+    failure ~error_message:"mkdir: cannot create directory ''"
   | Some (_q, (Here|Up)) ->
-    failure ~error_message:"mkdir: file exists" ~root ~root' (* CHECK *)
-  | Some (q, Down f) ->
-    let hintx = last_comp_as_hint ~root q in
-    let hinty = Feat.to_string f in [
+    failure ~error_message:"mkdir: file exists"
+  | Some (q, Down f) -> [
       success_case
         ~descr:(asprintf "mkdir %a: create directory" Path.pp p)
-        begin
+        begin fun root root' ->
+          let hintx = last_comp_as_hint ~root q in
+          let hinty = Feat.to_string f in
           exists2 ?hint1:hintx ?hint2:hintx @@ fun x x' ->
           exists ~hint:hinty @@ fun y ->
           resolve root cwd q x &
@@ -33,7 +33,8 @@ let interp_mkdir1 cwd path_str =
         end;
       error_case
         ~descr:(asprintf "mkdir %a: target already exists" Path.pp p)
-        begin
+        begin fun root root' ->
+          let hintx = last_comp_as_hint ~root q in
           exists ?hint:hintx @@ fun x ->
           resolve root cwd q x &
           dir x &
@@ -42,7 +43,8 @@ let interp_mkdir1 cwd path_str =
         end;
       error_case
         ~descr:(asprintf "mkdir %a: parent path is file or does not resolve" Path.pp p)
-        begin
+        begin fun root root' ->
+          let hintx = last_comp_as_hint ~root q in
           exists ?hint:hintx @@ fun x ->
           maybe_resolve root cwd q x
           & ndir x
diff --git a/src/symbolic/utilities/mv.ml b/src/symbolic/utilities/mv.ml
index a7e99563..d8dfd508 100644
--- a/src/symbolic/utilities/mv.ml
+++ b/src/symbolic/utilities/mv.ml
@@ -9,37 +9,35 @@ let name = "mv"
  *    used by 'mv'
  *)
 let interp_rename ctx src dstpath : utility =
-  under_specifications @@ fun ~root ~root' ->
-    let qsrc = Path.from_string src in
-    let qdst = Path.from_string dstpath in
+  let qsrc = Path.from_string src in
+  let qdst = Path.from_string dstpath in
+  under_specifications @@
     match Path.split_last qsrc, Path.split_last qdst with
     | (None, _) ->
-       failure ~error_message:"mv: invalid source path ''" ~root ~root'
+       failure ~error_message:"mv: invalid source path ''"
     | (_, None) ->
-       failure ~error_message:"mv: invalid destination path ''" ~root ~root'
+       failure ~error_message:"mv: invalid destination path ''"
     | (Some (_, (Here|Up)), _) | (_, Some(_, (Here|Up))) ->
-       failure ~error_message:"mv: paths end in . or .." ~root ~root'
+       failure ~error_message:"mv: paths end in . or .."
     | (Some (qs, Down fs), Some (qd, Down fd)) ->
-       let hintxs = last_comp_as_hint ~root qs in
-       let hintys = last_comp_as_hint ~root qsrc in
-       let hintxd = last_comp_as_hint ~root qd in
-       let hintyd = last_comp_as_hint ~root qdst in
        let unconditional_cases = [
            error_case
              ~descr:(asprintf "mv/rename: old '%s' does not resolve" src)
-             begin
+             begin fun root root' ->
                noresolve root ctx.cwd qsrc
                & eq root root'
              end;
            error_case
              ~descr:(asprintf "mv/rename: no path to new '%s'" dstpath)
-             begin
+             begin fun root root' ->
                noresolve root ctx.cwd qd
                & eq root root'
              end;
            success_case
              ~descr:(asprintf "mv/rename: same file")
-             begin
+             begin fun root root' ->
+               let hintys = last_comp_as_hint ~root qsrc in
+               let hintyd = last_comp_as_hint ~root qdst in
                exists2 ?hint1:hintys ?hint2:hintyd @@ fun ys yd ->
                resolve root ctx.cwd qsrc ys
                & resolve root ctx.cwd qdst yd
@@ -49,7 +47,9 @@ let interp_rename ctx src dstpath : utility =
            error_case
              ~descr:(asprintf "mv/rename: old '%s' is a directory, new '%s' is not"
                        src dstpath)
-             begin
+             begin fun root root' ->
+               let hintys = last_comp_as_hint ~root qsrc in
+               let hintyd = last_comp_as_hint ~root qdst in
                exists2 ?hint1:hintys ?hint2:hintyd @@ fun ys yd ->
                resolve root ctx.cwd qsrc ys & dir ys
                & resolve root ctx.cwd qdst yd & ndir yd
@@ -58,7 +58,11 @@ let interp_rename ctx src dstpath : utility =
            success_case
              ~descr:(asprintf "mv/rename: old '%s' is directory, new '%s' is an empty directory"
                        src dstpath)
-             begin
+             begin fun root root' ->
+               let hintxs = last_comp_as_hint ~root qs in
+               let hintys = last_comp_as_hint ~root qsrc in
+               let hintxd = last_comp_as_hint ~root qd in
+               let hintyd = last_comp_as_hint ~root qdst in
                exists2 ?hint1:hintxs ?hint2:hintys @@ fun xs ys ->
                exists2 ?hint1:hintyd ?hint2:None @@ fun yd xd' ->
                exists3 ?hint1:None ?hint2:hintxs ?hint3:hintxd @@ fun ri xsi xdi ->
@@ -75,7 +79,9 @@ let interp_rename ctx src dstpath : utility =
            error_case
              ~descr:(asprintf "mv/rename: old '%s' is directory, '%s' is not an empty directory"
                        src dstpath)
-             begin
+             begin fun root root' ->
+               let hintys = last_comp_as_hint ~root qsrc in
+               let hintyd = last_comp_as_hint ~root qdst in
                exists2 ?hint1:hintys ?hint2:hintyd @@ fun ys yd ->
                resolve root ctx.cwd qsrc ys & dir ys
                & resolve root ctx.cwd qdst yd & dir yd
@@ -85,7 +91,10 @@ let interp_rename ctx src dstpath : utility =
            success_case
              ~descr:(asprintf "mv/rename: old '%s' is file, new '%s' is absent"
                        src dstpath)
-             begin
+             begin fun root root' ->
+               let hintxs = last_comp_as_hint ~root qs in
+               let hintys = last_comp_as_hint ~root qsrc in
+               let hintxd = last_comp_as_hint ~root qd in
                exists2 ?hint1:hintxs ?hint2:hintys @@ fun xs ys ->
                exists2 ?hint1:hintxd ?hint2:None @@ fun xd xd' ->
                exists3 ?hint1:None ?hint2:hintxs ?hint3:hintxd @@ fun ri xsi xdi ->
@@ -102,7 +111,11 @@ let interp_rename ctx src dstpath : utility =
            success_case
              ~descr:(asprintf "mv/rename: old '%s' is file, new '%s' is not directory"
                        src dstpath)
-             begin
+             begin fun root root' ->
+              let hintxs = last_comp_as_hint ~root qs in
+              let hintys = last_comp_as_hint ~root qsrc in
+              let hintxd = last_comp_as_hint ~root qd in
+              let hintyd = last_comp_as_hint ~root qdst in
               exists2 ?hint1:hintxs ?hint2:hintys @@ fun xs ys ->
               exists3 ?hint1:hintxd ?hint2:hintyd ?hint3:None @@ fun xd yd xd' ->
               exists3 ?hint1:None ?hint2:None ?hint3:None @@ fun ri xsi xdi ->
@@ -119,7 +132,9 @@ let interp_rename ctx src dstpath : utility =
            error_case
              ~descr:(asprintf "mv/rename: old '%s' is a file, new '%s' is a directory"
                        src dstpath)
-            begin
+            begin fun root root' ->
+              let hintys = last_comp_as_hint ~root qsrc in
+              let hintyd = last_comp_as_hint ~root qdst in
               exists2 ?hint1:hintys ?hint2:hintyd @@ fun ys yd ->
               resolve root ctx.cwd qsrc ys & ndir ys
               & resolve root ctx.cwd qdst yd & dir yd
@@ -136,7 +151,9 @@ let interp_rename ctx src dstpath : utility =
            error_case
              ~descr:(asprintf "mv/rename: old '%s' is ancestor of new '%s'"
                      src dstpath)
-             begin
+             begin fun root root' ->
+               let hintys = last_comp_as_hint ~root qsrc in
+               let hintxd = last_comp_as_hint ~root qd in
                exists2 ?hint1:hintys ?hint2:hintxd @@ fun ys xd ->
                resolve root ctx.cwd qsrc ys & dir ys
                & resolve root ctx.cwd qd xd
@@ -153,7 +170,9 @@ let interp_rename ctx src dstpath : utility =
              error_case
                ~descr:(asprintf "old '%s' is directory, new '%s' is absent and slash"
                          src dstpath)
-               begin
+               begin fun root root' ->
+                 let hintys = last_comp_as_hint ~root qsrc in
+                 let hintxd = last_comp_as_hint ~root qd in
                  exists2 ?hint1:hintys ?hint2:hintxd @@ fun ys xd ->
                  resolve root ctx.cwd qsrc ys & dir ys
                  & resolve root ctx.cwd qd xd
@@ -166,7 +185,10 @@ let interp_rename ctx src dstpath : utility =
              success_case
                ~descr:(asprintf "old '%s' is directory, new '%s' is absent"
                      src dstpath)
-               begin
+               begin fun root root' ->
+                 let hintxs = last_comp_as_hint ~root qs in
+                 let hintys = last_comp_as_hint ~root qsrc in
+                 let hintxd = last_comp_as_hint ~root qd in
                  exists2 ?hint1:hintxs ?hint2:hintys @@ fun xs ys ->
                  exists2 ?hint1:hintxd ?hint2:None @@ fun xd xd' ->
                  exists3 ?hint1:None ?hint2:None ?hint3:None @@ fun ri xsi xdi ->
diff --git a/src/symbolic/utilities/rm.ml b/src/symbolic/utilities/rm.ml
index 5d283ab8..b522c014 100644
--- a/src/symbolic/utilities/rm.ml
+++ b/src/symbolic/utilities/rm.ml
@@ -6,21 +6,21 @@ open SymbolicUtility
 let name = "rm"
 
 let interp1 cwd arg : utility =
-  under_specifications @@ fun ~root ~root' ->
   let oq = Path.from_string arg in
+  under_specifications @@
   match Path.split_last oq with
   (* FIXME: Here, I reuse the same programming scheme as in mkdir. *)
   (* FIXME: Shouldn't we factorize it in a combinator?             *)
   | None ->
-    failure ~error_message:"rm: invalid path ''" ~root ~root'
+    failure ~error_message:"rm: invalid path ''"
   | Some (_q, (Here|Up)) ->
-    failure ~error_message:"rm: cannot remove .. or ." ~root ~root'
-  | Some (q, Down f) ->
-    let hintx = last_comp_as_hint ~root q in
-    let hinty = Feat.to_string f in [
+    failure ~error_message:"rm: cannot remove .. or ."
+  | Some (q, Down f) -> [
       success_case
         ~descr:(asprintf "rm %a: remove file" Path.pp oq)
-        begin
+        begin fun root root' ->
+          let hintx = last_comp_as_hint ~root q in
+          let hinty = Feat.to_string f in
           exists2 ?hint1:hintx ?hint2:hintx @@ fun x x' ->
           exists ~hint:hinty @@ fun y ->
           resolve root cwd oq y & ndir y
@@ -30,7 +30,8 @@ let interp1 cwd arg : utility =
         end;
       error_case
         ~descr:(asprintf "rm %a: target does not exist or is a directory" Path.pp oq)
-        begin
+        begin fun root root' ->
+          let hinty = Feat.to_string f in
           exists ~hint:hinty @@ fun y ->
           maybe_resolve root cwd oq y
           & dir y
@@ -39,21 +40,21 @@ let interp1 cwd arg : utility =
     ]
 
 let interp1_r cwd arg : utility =
-  under_specifications @@ fun ~root ~root' ->
   let oq = Path.from_string arg in
+  under_specifications @@
   match Path.split_last oq with
   (* FIXME: Here, I reuse the same programming scheme as in mkdir. *)
   (* FIXME: Shouldn't we factorize it in a combinator?             *)
   | None ->
-    failure ~error_message:"rm: invalid path ''" ~root ~root'
+    failure ~error_message:"rm: invalid path ''"
   | Some (_q, (Here|Up)) ->
-    failure ~error_message:"rm: cannot remove .. or ." ~root ~root'
-  | Some (q, Down f) ->
-    let hintx = last_comp_as_hint ~root q in
-    let hinty = Feat.to_string f in [
+    failure ~error_message:"rm: cannot remove .. or ."
+  | Some (q, Down f) -> [
       success_case
         ~descr:(asprintf "rm -r %a: remove file or directory" Path.pp oq)
-        begin
+        begin fun root root' ->
+          let hintx = last_comp_as_hint ~root q in
+          let hinty = Feat.to_string f in
           exists2 ?hint1:hintx ?hint2:hintx @@ fun x x' ->
           exists ~hint:hinty @@ fun y ->
           resolve root cwd oq y
@@ -63,7 +64,7 @@ let interp1_r cwd arg : utility =
         end;
       error_case
         ~descr:(asprintf "rm -r %a: target does not exist" Path.pp oq)
-        begin
+        begin fun root root' ->
           noresolve root cwd oq & eq root root'
         end;
     ]
diff --git a/src/symbolic/utilities/test.ml b/src/symbolic/utilities/test.ml
index b9a58741..9ffb1d98 100644
--- a/src/symbolic/utilities/test.ml
+++ b/src/symbolic/utilities/test.ml
@@ -11,41 +11,31 @@ let name = "test"
 (******************************************************************************)
 
 let interp_test_parse_error args : utility =
-  under_specifications @@ fun ~root ~root' ->
-  [
+  under_specifications [
     let descr = "test: parse error in `" ^ (String.concat " " args) ^ "`" in
-    error_case
-      ~descr
-      begin
-        eq root root'
-      end;
+    error_case ~descr noop
   ]
 
 let interp_test_empty () : utility =
-  under_specifications @@ fun ~root ~root' ->
-  [
+  under_specifications [
     let descr = "test: empty expression" in
-    error_case
-      ~descr
-      begin
-        eq root root'
-      end;
+    error_case ~descr noop
   ]
 
 let interp_test_e cwd path_str : utility =
-  under_specifications @@ fun ~root ~root' ->
   let p = Path.from_string path_str in
-  let hintx = last_comp_as_hint ~root p in [
+  under_specifications [
     success_case
       ~descr:(asprintf "test -e %a: path resolves" Path.pp p)
-      begin
+      begin fun root root' ->
+        let hintx = last_comp_as_hint ~root p in
         exists ?hint:hintx @@ fun x ->
         resolve root cwd p x &
         eq root root'
       end;
     error_case
       ~descr:(asprintf "test -e %a: path does not resolve" Path.pp p)
-      begin
+      begin fun root root' ->
         noresolve root cwd p &
         eq root root'
       end;
@@ -106,19 +96,20 @@ let interp_test_f cwd path_str : utility =
  *)
 
 let interp_test_file_type ~attr is_type is_ntype cwd path_str : utility =
-  under_specifications @@ fun ~root ~root' ->
   let p = Path.from_string path_str in
-  let hintx = last_comp_as_hint ~root p in [
+  under_specifications [
     success_case
       ~descr:(asprintf "test -%s %a: path resolves to file of type '%s'" attr Path.pp p attr)
-      begin
+      begin fun root root' ->
+        let hintx = last_comp_as_hint ~root p in
         exists ?hint:hintx @@ fun x ->
         resolve root cwd p x & is_type x &
         eq root root'
       end;
     error_case
       ~descr:(asprintf "test -%s %a: path does not resolve or to file of type other than '%s'" attr Path.pp p attr)
-      begin
+      begin fun root root' ->
+        let hintx = last_comp_as_hint ~root p in
         exists ?hint:hintx @@ fun x ->
         maybe_resolve root cwd p x
         & is_ntype x
@@ -127,98 +118,80 @@ let interp_test_file_type ~attr is_type is_ntype cwd path_str : utility =
   ]
 
 let interp_test_attribute ~attr cwd path_str : utility =
-  under_specifications @@ fun ~root ~root' ->
   let p = Path.from_string path_str in
-  let hintx = last_comp_as_hint ~root p in [
+  under_specifications [
     success_case
       ~descr:(asprintf "test '%a': path resolves, attribute -%s OK (overapprox to -e)"
                 Path.pp p attr)
-      begin
+      begin fun root root' ->
+        let hintx = last_comp_as_hint ~root p in
         exists ?hint:hintx @@ fun x ->
         resolve root cwd p x &
         eq root root'
       end;
     error_case
       ~descr:(asprintf "test '%a': path does not resolve or resolves but attribute -%s not OK (overapprox to -e)" Path.pp p attr)
-      begin
-        eq root root'
-      end;
+      noop
   ]
 
 let interp_test_n str : utility =
-  under_specifications @@ fun ~root ~root' ->
+  under_specifications @@
   if str = "" then
     [
       error_case
         ~descr:(asprintf "test -n '%s': string is empty" str)
-      begin
-        eq root root'
-      end
+        noop
     ]
   else
     [
       success_case
         ~descr:(asprintf "test -n '%s': string is non-empty" str)
-      begin
-        eq root root'
-      end
+        noop
     ]
 
 let interp_test_z str : utility =
-  under_specifications @@ fun ~root ~root' ->
+  under_specifications @@
   if str = "" then
     [
       success_case
         ~descr:(asprintf "test -z '%s': string is empty" str)
-      begin
-        eq root root'
-      end
+        noop
     ]
   else
     [
       error_case
         ~descr:(asprintf "test -z '%s': string is non-empty" str)
-      begin
-        eq root root'
-      end
+        noop
     ]
 
 let interp_test_string_equal s1 s2 : utility =
-  under_specifications @@ fun ~root ~root' ->
+  under_specifications @@
   if s1 = s2 then
     [
       success_case
         ~descr:(asprintf "test '%s' = '%s': strings are equal" s1 s2)
-      begin
-        eq root root'
-      end
+        noop
     ]
   else
     [
       error_case
         ~descr:(asprintf "test '%s' = '%s': string are not equal" s1 s2)
-      begin
-        eq root root'
-      end
+        noop
     ]
 
 let interp_test_string_notequal s1 s2 : utility =
-  under_specifications @@ fun ~root ~root' ->
+  under_specifications @@
   if s1 <> s2 then
     [
       success_case
         ~descr:(asprintf "test '%s' != '%s': strings are not equal" s1 s2)
-      begin
-        eq root root'
-      end
+        noop
     ]
   else
     [
       error_case
         ~descr:(asprintf "test '%s' != '%s': string are equal" s1 s2)
-      begin
-        eq root root'
-      end
+        noop
     ]
 
 let rec interp_test_expr cwd e : utility =
diff --git a/src/symbolic/utilities/touch.ml b/src/symbolic/utilities/touch.ml
index 7a170137..806c7778 100644
--- a/src/symbolic/utilities/touch.ml
+++ b/src/symbolic/utilities/touch.ml
@@ -8,40 +8,41 @@ let name = "touch"
 let interp_touch1 cwd path_str : utility =
   (* FIXME: we can merge two cases here (parent path does not resolve & parent
      path isn't a directory) *)
-  under_specifications @@ fun ~root ~root' ->
   let p = Path.from_string path_str in
+  under_specifications @@
   match Path.split_last p with
   | None -> (* `touch ''` *)
-    failure ~error_message:"cannot touch '': No such file or directory" ~root ~root'
-  | Some (q, (Up | Here)) ->
-    let hint = last_comp_as_hint ~root p in [
+    failure ~error_message:"cannot touch '': No such file or directory"
+  | Some (_, (Up | Here)) -> [
       success_case
         ~descr:(asprintf "touch %a: path resolves" Path.pp p)
-        begin
+        begin fun root root' ->
+          let hint = last_comp_as_hint ~root p in
           exists ?hint @@ fun y ->
           resolve root cwd p y &
           eq root root'
         end;
       error_case
         ~descr:(asprintf "touch %a: path does not resolve" Path.pp p)
-        begin
+        begin fun root root' ->
           noresolve root cwd p &
           eq root root'
         end
     ]
-  | Some (q, Down f) ->
-    let hintx = last_comp_as_hint ~root q in
-    let hinty = Feat.to_string f in [
+  | Some (q, Down f) -> [
       success_case
         ~descr:(asprintf "touch %a: path resolves" Path.pp p)
-        begin
+        begin fun root root' ->
+          let hinty = Feat.to_string f in
           exists ~hint:hinty @@ fun y ->
           resolve root cwd p y &
           eq root root'
         end;
       success_case
         ~descr:(asprintf "touch %a: create file" Path.pp p)
-        begin
+        begin fun root root' ->
+          let hintx = last_comp_as_hint ~root q in
+          let hinty = Feat.to_string f in
           exists3 ?hint1:hintx ?hint2:hintx ~hint3:hinty @@ fun x x' y' ->
           resolve root cwd q x &
           dir x &
@@ -54,7 +55,8 @@ let interp_touch1 cwd path_str : utility =
         end;
       error_case
         ~descr:(asprintf "touch %a: parent path does not resolve or resolves to dir" Path.pp p)
-        begin
+        begin fun root root' ->
+          let hintx = last_comp_as_hint ~root q in
           exists ?hint:hintx @@ fun x ->
           maybe_resolve root cwd q x
           & ndir x
diff --git a/src/symbolic/utilities/which.ml b/src/symbolic/utilities/which.ml
index 619c44b5..1f964908 100644
--- a/src/symbolic/utilities/which.ml
+++ b/src/symbolic/utilities/which.ml
@@ -9,19 +9,14 @@ module Silent = struct
 
   let interprete _ctx = function
     | [p] ->
-      under_specifications @@ fun ~root ~root' ->
-      [
+      under_specifications [
         success_case
           ~descr:(asprintf "silent-which '%s': assuming command is found" p)
-          begin
-            eq root root'
-          end
+          noop
         ;
         error_case
           ~descr:(asprintf "silent-which '%s': assuming command is not found" p)
-          begin
-            eq root root'
-          end
+          noop
       ]
     | _ ->
       unsupported ~utility:"silent-which" "more than one argument"
@@ -36,26 +31,27 @@ end
 let name = "which"
 
 let interp_test_regular_and_x cwd path_str : utility =
-  under_specifications @@ fun ~root ~root' ->
   let p = Path.from_string path_str in
-  let hintx = last_comp_as_hint ~root p in [
+  under_specifications [
     success_case
       ~descr:(asprintf "which '%a': path resolves to a regular executable (overapprox to -f)" Path.pp p)
       ~stdout:Stdout.(empty |> output (asprintf "%a" Path.pp p) |> newline)
-      begin
+      begin fun root root' ->
+        let hintx = last_comp_as_hint ~root p in
         exists ?hint:hintx @@ fun x ->
         resolve root cwd p x & reg x & (* no way to constraint "x" mode *)
         eq root root'
       end;
     error_case
       ~descr:(asprintf "which '%a': path does not resolve" Path.pp p)
-      begin
+      begin fun root root' ->
         noresolve root cwd p &
         eq root root'
       end;
     error_case
       ~descr:(asprintf "which '%a': path resolves but not to regular executable)" Path.pp p)
-      begin
+      begin fun root root' ->
+        let hintx = last_comp_as_hint ~root p in
         exists ?hint:hintx @@ fun x ->
         resolve root cwd p x & (* no way to constraint no "x" mode *)
         eq root root'
@@ -66,13 +62,10 @@ let interp_test_regular_and_x cwd path_str : utility =
 let rec search_as_which_in_path cwd (path:string list) arg : utility =
   match path with
   | [] ->
-    under_specifications @@ fun ~root ~root' ->
-    [
+    under_specifications [
       error_case
         ~descr:(asprintf "which: `%s` not found in PATH" arg)
-        begin
-          eq root root'
-        end
+        noop
     ]
   | p :: rem ->
     let u1 = interp_test_regular_and_x cwd (p ^ "/" ^ arg) in