diff --git a/lib/lin.ml b/lib/lin.ml
index 6a1fb7609..61e79813a 100644
--- a/lib/lin.ml
+++ b/lib/lin.ml
@@ -3,6 +3,27 @@ struct
   open QCheck
   include Util
 
+  module Var =
+  struct
+    type t = int
+    let next, reset =
+      let counter = ref 0 in
+      (fun () -> let old = !counter in
+        incr counter; old),
+      (fun () -> counter := 0)
+    let show v = Format.sprintf "t%i" v
+    let pp fmt v = Format.fprintf fmt "%s" (show v)
+  end
+
+  module Env =
+  struct
+    type t = Var.t list
+    let gen_t_var env = Gen.oneofl env
+    let valid_t_vars env v =
+      if v = 0 then Iter.empty else
+        Iter.of_list (List.rev (List.filter (fun v' -> v' < v) env))
+  end
+
   module type CmdSpec = sig
     type t
     (** The type of the system under test *)
@@ -13,12 +34,18 @@ struct
     val show_cmd : cmd -> string
     (** [show_cmd c] returns a string representing the command [c]. *)
 
-    val gen_cmd : cmd Gen.t
-    (** A command generator. *)
+    val gen_cmd : Var.t Gen.t -> (Var.t option * cmd) Gen.t
+    (** A command generator.
+        It accepts a variable generator and generates a pair [(opt,cmd)] with the option indicating
+        an storage index to store the [cmd]'s result. *)
 
-    val shrink_cmd : cmd Shrink.t
+    val shrink_cmd : Env.t -> cmd Shrink.t
     (** A command shrinker.
-        To a first approximation you can use [Shrink.nil]. *)
+        It accepts the current environment as its argument.
+        To a first approximation you can use [fun _env -> Shrink.nil]. *)
+
+    val cmd_uses_var : Var.t -> cmd -> bool
+    (** [cmd_uses_var v cmd] should return [true] iff the command [cmd] refers to the variable [v]. *)
 
     type res
     (** The command result type *)
@@ -35,88 +62,170 @@ struct
     (** Utility function to clean up [t] after each test instance,
         e.g., for closing sockets, files, or resetting global parameters *)
 
-    val run : cmd -> t -> res
-    (** [run c t] should interpret the command [c] over the system under test [t] (typically side-effecting). *)
-  end
+    val run : (Var.t option * cmd) -> t array -> res
+    (** [run (opt,c) t] should interpret the command [c] over the various instances of the system under test [t array] (typically side-effecting).
+        [opt] indicates the index to store the result. *)
+end
+
+  type 'cmd cmd_triple =
+    { env_size   : int;
+      seq_prefix : (Var.t option * 'cmd) list;
+      tail_left  : (Var.t option * 'cmd) list;
+      tail_right : (Var.t option * 'cmd) list; }
+
 
   (** A functor to create test setups, for all backends (Domain, Thread and Effect).
       We use it below, but it can also be used independently *)
   module Make(Spec : CmdSpec)
   = struct
-
     (* plain interpreter of a cmd list *)
     let interp_plain sut cs = List.map (fun c -> (c, Spec.run c sut)) cs
 
-    let rec gen_cmds fuel =
+    (* val gen_cmds : Env.t -> int -> (Env.t * (Var.t option * Spec.cmd) list) Gen.t *)
+    let rec gen_cmds env fuel =
       Gen.(if fuel = 0
-           then return []
+           then return (env,[])
            else
-             Spec.gen_cmd >>= fun c ->
-             gen_cmds (fuel-1) >>= fun cs ->
-             return (c::cs))
-    (** A fueled command list generator. *)
-
-    let gen_cmds_size size_gen = Gen.sized_size size_gen gen_cmds
-
-    let shrink_triple (seq,p1,p2) =
+             Spec.gen_cmd (Env.gen_t_var env) >>= fun (opt,c) ->
+               let env = match opt with None -> env | Some v -> v::env in
+               gen_cmds env (fuel-1) >>= fun (env,cs) -> return (env,(opt,c)::cs))
+    (** A fueled command list generator.
+        Accepts an environment parameter [env] to enable [cmd] generation of multiple [t]s
+        and returns the extended environment. *)
+
+    let gen_cmds_size env size_gen = Gen.sized_size size_gen (gen_cmds env)
+
+    (* Note that the result is built in reverse (ie should be
+       _decreasing_) order *)
+    let rec extract_env env cmds =
+      match cmds with
+      | []                  -> env
+      | (Some i, _) :: cmds -> extract_env (i::env) cmds
+      | (None,   _) :: cmds -> extract_env     env  cmds
+
+    let cmds_use_var var cmds =
+      List.exists (fun (_,c) -> Spec.cmd_uses_var var c) cmds
+
+    let ctx_doesnt_use_var _var = false
+
+    let rec shrink_cmd_list_spine cmds ctx_uses_var = match cmds with
+      | [] -> Iter.empty
+      | c::cs ->
+        let open Iter in
+        (match fst c with
+         | None -> (* shrink tail first as fewer other vars should depend on it *)
+           (map (fun cs -> c::cs) (shrink_cmd_list_spine cs ctx_uses_var)
+            <+>
+            return cs) (* not a t-assignment, so try without it *)
+         | Some i -> (* shrink tail first as fewer other vars should depend on it *)
+           (map (fun cs -> c::cs) (shrink_cmd_list_spine cs ctx_uses_var)
+           <+>
+           if cmds_use_var i cs || ctx_uses_var i
+           then empty
+           else return cs)) (* t_var not used, so try without it *)
+
+    let rec shrink_individual_cmds env cmds = match cmds with
+      | [] -> Iter.empty
+      | (opt,cmd) :: cmds ->
+        let env' = match opt with None -> env | Some i -> i::env in
+        let open Iter in
+        map (fun cmds -> (opt,cmd)::cmds) (shrink_individual_cmds env' cmds)
+        <+>
+        map (fun cmd -> (opt,cmd)::cmds) (Spec.shrink_cmd env cmd)
+
+    let shrink_triple ({ env_size=_; seq_prefix=seq; tail_left=p1; tail_right=p2 } as t) =
       let open Iter in
       (* Shrinking heuristic:
          First reduce the cmd list sizes as much as possible, since the interleaving
          is most costly over long cmd lists. *)
-      (map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq))
+      map (fun seq -> { t with seq_prefix=seq }) (shrink_cmd_list_spine seq (fun var -> cmds_use_var var p1 || cmds_use_var var p2))
       <+>
-      (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2))
+      map (fun p1 -> { t with tail_left=p1 }) (shrink_cmd_list_spine p1 ctx_doesnt_use_var)
       <+>
-      (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s))
+      map (fun p2 -> { t with tail_right=p2 }) (shrink_cmd_list_spine p2 ctx_doesnt_use_var)
+      <+> (* eta-expand the following two to lazily compute the match and @ until/if needed *)
+      (fun yield -> (match p1 with [] -> Iter.empty | c1::c1s -> Iter.return { t with seq_prefix=seq@[c1]; tail_left=c1s}) yield)
       <+>
-      (map (fun p1' -> (seq,p1',p2)) (Shrink.list_spine p1))
-      <+>
-      (map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2))
+      (fun yield -> (match p2 with [] -> Iter.empty | c2::c2s -> Iter.return { t with seq_prefix=seq@[c2]; tail_right=c2s}) yield)
       <+>
       (* Secondly reduce the cmd data of individual list elements *)
-      (map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems Spec.shrink_cmd seq))
-      <+>
-      (map (fun p1' -> (seq,p1',p2)) (Shrink.list_elems Spec.shrink_cmd p1))
+      (fun yield ->
+         let seq_env = extract_env [0] seq in (* only extract_env if needed *)
+         (Iter.map (fun p1 -> { t with tail_left=p1 }) (shrink_individual_cmds seq_env p1)
+          <+>
+          Iter.map (fun p2 -> { t with tail_right=p2 }) (shrink_individual_cmds seq_env p2))
+           yield)
       <+>
-      (map (fun p2' -> (seq,p1,p2')) (Shrink.list_elems Spec.shrink_cmd p2))
+      Iter.map (fun seq -> { t with seq_prefix=seq }) (shrink_individual_cmds [0] seq)
+
+    let show_cmd (opt,c) = match opt with
+      | None   -> Spec.show_cmd c
+      | Some v -> Printf.sprintf "let %s = %s" (Var.show v) (Spec.show_cmd c)
+
+    let init_cmd = "let t0 = init ()"
+    let init_cmd_ret = init_cmd ^ " : ()"
+
+    let print_triple { seq_prefix; tail_left; tail_right; _ } =
+      print_triple_vertical ~init_cmd show_cmd (seq_prefix, tail_left, tail_right)
 
     let arb_cmds_triple seq_len par_len =
-      let gen_triple =
+      let gen_triple st =
+        Var.reset ();
+        let init_var = Var.next () in
+        assert (init_var = 0);
         Gen.(int_range 2 (2*par_len) >>= fun dbl_plen ->
-             let seq_pref_gen = gen_cmds_size (int_bound seq_len) in
              let par_len1 = dbl_plen/2 in
-             let par_gen1 = gen_cmds_size (return par_len1) in
-             let par_gen2 = gen_cmds_size (return (dbl_plen - par_len1)) in
-             triple seq_pref_gen par_gen1 par_gen2) in
-      make ~print:(print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple
-
-    let rec check_seq_cons pref cs1 cs2 seq_sut seq_trace = match pref with
+             gen_cmds_size [init_var] (int_bound seq_len) >>= fun (env,seq_prefix) ->
+             gen_cmds_size env (return par_len1) >>= fun (_env1,tail_left) ->
+             gen_cmds_size env (return (dbl_plen - par_len1)) >>= fun (_env2,tail_right) ->
+             let env_size = Var.next () in
+             return { env_size; seq_prefix; tail_left; tail_right }) st
+      in
+      make ~print:print_triple ~shrink:shrink_triple gen_triple
+
+    let init_sut array_size =
+      let sut = Spec.init () in
+      Array.make array_size sut
+
+    let cleanup sut seq_pref cmds1 cmds2 =
+      let cleanup_opt (opt,_c) = match opt with
+        | None -> ()
+        | Some v -> Spec.cleanup sut.(v) in
+      Spec.cleanup sut.(0); (* always present *)
+      List.iter cleanup_opt seq_pref;
+      List.iter cleanup_opt cmds1;
+      List.iter cleanup_opt cmds2
+
+    let cleanup_traces sut seq_pref cmds1 cmds2 =
+      cleanup sut (List.map fst seq_pref) (List.map fst cmds1) (List.map fst cmds2)
+
+    let rec check_seq_cons array_size pref cs1 cs2 seq_sut seq_trace = match pref with
       | (c,res)::pref' ->
         if Spec.equal_res res (Spec.run c seq_sut)
-        then check_seq_cons pref' cs1 cs2 seq_sut (c::seq_trace)
-        else (Spec.cleanup seq_sut; false)
+        then check_seq_cons array_size pref' cs1 cs2 seq_sut (c::seq_trace)
+        else (cleanup_traces seq_sut pref cs1 cs2; false)
       (* Invariant: call Spec.cleanup immediately after mismatch  *)
       | [] -> match cs1,cs2 with
-        | [],[] -> Spec.cleanup seq_sut; true
+        | [],[] -> cleanup_traces seq_sut pref cs1 cs2; true
         | [],(c2,res2)::cs2' ->
           if Spec.equal_res res2 (Spec.run c2 seq_sut)
-          then check_seq_cons pref cs1 cs2' seq_sut (c2::seq_trace)
-          else (Spec.cleanup seq_sut; false)
+          then check_seq_cons array_size pref cs1 cs2' seq_sut (c2::seq_trace)
+          else (cleanup_traces seq_sut pref cs1 cs2; false)
         | (c1,res1)::cs1',[] ->
           if Spec.equal_res res1 (Spec.run c1 seq_sut)
-          then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace)
-          else (Spec.cleanup seq_sut; false)
+          then check_seq_cons array_size pref cs1' cs2 seq_sut (c1::seq_trace)
+          else (cleanup_traces seq_sut pref cs1 cs2; false)
         | (c1,res1)::cs1',(c2,res2)::cs2' ->
           (if Spec.equal_res res1 (Spec.run c1 seq_sut)
-           then check_seq_cons pref cs1' cs2 seq_sut (c1::seq_trace)
-           else (Spec.cleanup seq_sut; false))
+           then check_seq_cons array_size pref cs1' cs2 seq_sut (c1::seq_trace)
+           else (cleanup_traces seq_sut pref cs1 cs2; false))
           ||
           (* rerun to get seq_sut to same cmd branching point *)
-          (let seq_sut' = Spec.init () in
+          (let seq_sut' = init_sut array_size in
            let _ = interp_plain seq_sut' (List.rev seq_trace) in
            if Spec.equal_res res2 (Spec.run c2 seq_sut')
-           then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace)
-           else (Spec.cleanup seq_sut'; false))
+           then check_seq_cons array_size pref cs1 cs2' seq_sut' (c2::seq_trace)
+           else (cleanup_traces seq_sut' pref cs1 cs2; false))
 
     (* Linearization test *)
     let lin_test ~rep_count ~retries ~count ~name ~lin_prop =
@@ -192,6 +301,14 @@ let array : type a c s. (a, c, s, combinable) ty -> (a array, c, s, combinable)
     | GenDeconstr (arb, print, eq) -> GenDeconstr (QCheck.array arb, QCheck.Print.array print, Array.for_all2 eq)
     | Deconstr (print, eq) -> Deconstr (QCheck.Print.array print, Array.for_all2 eq)
 
+let bounded_array : type a c s. int -> (a, c, s, combinable) ty -> (a array, c, s, combinable) ty =
+  fun maxsize ty ->
+  let array = QCheck.array_of_size (QCheck.Gen.int_bound maxsize) in
+  match ty with
+  | Gen (arb, print) -> Gen (array arb, QCheck.Print.array print)
+  | GenDeconstr (arb, print, eq) -> GenDeconstr (array arb, QCheck.Print.array print, Array.for_all2 eq)
+  | Deconstr (print, eq) -> Deconstr (QCheck.Print.array print, Array.for_all2 eq)
+
 let print_seq pp s =
   let b = Buffer.create 25 in
   Buffer.add_char b '<';
@@ -294,7 +411,7 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
       | Ret_ignore : ('a, _, t, _) ty -> ('a, unit) args
       | Ret_ignore_or_exc : ('a, _, t, _) ty -> ('a, (unit,exn) result) args
       | Fn : 'a * ('b,'r) args -> ('a -> 'b, 'r) args
-      | FnState : ('b,'r) args -> (t -> 'b, 'r) args
+      | FnState : Internal.Var.t * ('b,'r) args -> (t -> 'b, 'r) args
   end
 
   (* Operation name, typed argument list, return type descriptor, printer, shrinker, function *)
@@ -315,8 +432,8 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
   (* Function to generate typed list of arguments from a function description.
      The printer can be generated independently. *)
   let rec gen_args_of_desc
-    : type a r. (a, r, t) Fun.fn -> ((a, r) Args.args) QCheck.Gen.t =
-    fun fdesc ->
+    : type a r. (a, r, t) Fun.fn -> (Internal.Var.t QCheck.Gen.t) -> ((a, r) Args.args) QCheck.Gen.t =
+    fun fdesc gen_var ->
     let open QCheck.Gen in
     match fdesc with
     | Fun.Ret ty -> return @@ Args.Ret ty
@@ -324,28 +441,37 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
     | Fun.Ret_ignore_or_exc ty -> return @@ Args.Ret_ignore_or_exc ty
     | Fun.Ret_ignore ty -> return @@ Args.Ret_ignore ty
     | Fun.(Fn (State, fdesc_rem)) ->
-      let* args_rem = gen_args_of_desc fdesc_rem in
-      return @@ Args.FnState args_rem
+        map2 (fun state_arg args_rem -> Args.FnState (state_arg, args_rem))
+          gen_var (gen_args_of_desc fdesc_rem gen_var)
+     (* let* state_arg = gen_var in
+        let* args_rem = gen_args_of_desc fdesc_rem gen_var in
+        return @@ Args.FnState (state_arg, args_rem) *)
     | Fun.(Fn ((Gen (arg_arb,_) | GenDeconstr (arg_arb, _, _)), fdesc_rem)) ->
-      let* arg = arg_arb.gen in
-      let* args_rem = gen_args_of_desc fdesc_rem in
-      return @@ Args.Fn (arg, args_rem)
+        map2 (fun arg args_rem -> Args.Fn (arg, args_rem))
+          arg_arb.gen (gen_args_of_desc fdesc_rem gen_var)
+     (* let* arg = arg_arb.gen in
+        let* args_rem = gen_args_of_desc fdesc_rem gen_var in
+        return @@ Args.Fn (arg, args_rem) *)
 
   let rec ret_type
-    : type a r. (a,r,t) Fun.fn -> (r, deconstructible, t, _) ty
+    : type a r. (a,r,t) Fun.fn -> Internal.Var.t option * (r, deconstructible, t, _) ty
     = fun fdesc ->
       match fdesc with
-      | Fun.Ret ty -> ty
-      | Fun.Ret_or_exc ty -> or_exn ty
-      | Fun.Ret_ignore _ -> unit
-      | Fun.Ret_ignore_or_exc _ -> or_exn unit
+      | Fun.Ret ty -> None, ty
+      | Fun.Ret_or_exc ty -> None, or_exn ty
+      | Fun.Ret_ignore ty -> (match ty with
+          | State -> Some (Internal.Var.next ()), unit
+          | _     -> None, unit)
+      | Fun.Ret_ignore_or_exc ty -> (match ty with
+          | State -> Some (Internal.Var.next ()), or_exn unit
+          | _     -> None, or_exn unit)
       | Fun.Fn (_, fdesc_rem) -> ret_type fdesc_rem
 
   let rec show_args : type a r. (a,r,t) Fun.fn -> (a,r) Args.args -> string list = fun fdesc args ->
     match fdesc,args with
     | _, Args.(Ret _ | Ret_or_exc _ | Ret_ignore _ | Ret_ignore_or_exc _) -> []
-    | Fun.(Fn (State, fdesc_rem)), Args.(FnState args_rem) ->
-      "t"::show_args fdesc_rem args_rem
+    | Fun.(Fn (State, fdesc_rem)), Args.(FnState (index,args_rem)) ->
+        (Internal.Var.show index)::(show_args fdesc_rem args_rem)
     | Fun.(Fn ((GenDeconstr _ | Gen _ as ty), fdesc_rem)), Args.(Fn (value, args_rem)) ->
       (print ty value)::show_args fdesc_rem args_rem
     | Fun.(Fn (State, _)), Args.(Fn _)
@@ -368,9 +494,9 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
     | Fun.Ret_ignore_or_exc _ty -> Shrink.nil
     | Fun.Ret_ignore _ty -> Shrink.nil
     | Fun.(Fn (State, fdesc_rem)) ->
-      (function (Args.FnState args) ->
-         Iter.map (fun args -> Args.FnState args) (gen_shrinker_of_desc fdesc_rem args)
-              | _ -> failwith "FnState: should not happen")
+        (function (Args.FnState (index,args)) ->
+          Iter.map (fun args -> Args.FnState (index,args)) (gen_shrinker_of_desc fdesc_rem args)
+                | _ -> failwith "FnState: should not happen")
     | Fun.(Fn ((Gen (arg_arb,_) | GenDeconstr (arg_arb, _, _)), fdesc_rem)) ->
       (match arg_arb.shrink with
        | None ->
@@ -384,21 +510,46 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
              (map (fun args -> Args.Fn (a,args)) (gen_shrinker_of_desc fdesc_rem args))
                       | _ -> failwith "Fn/Some: should not happen"))
 
-  let api =
+  let api gen_t_var =
     List.map (fun (wgt, Elem { name ; fntyp = fdesc ; value = f }) ->
-        let rty = ret_type fdesc in
+        let print = gen_printer name fdesc in
+        let shrink = gen_shrinker_of_desc fdesc in
         let open QCheck.Gen in
-        (wgt, gen_args_of_desc fdesc >>= fun args ->
-         let print = gen_printer name fdesc in
-         let shrink = gen_shrinker_of_desc fdesc in
-         return (Cmd { name ; args ; rty ; print ; shrink ; f }))) ApiSpec.api
+        (wgt, gen_args_of_desc fdesc gen_t_var >>= fun args ->
+          let opt_var, rty = ret_type fdesc in
+          return (opt_var, Cmd { name ; args ; rty ; print ; shrink ; f }))) ApiSpec.api
 
-  let gen_cmd : cmd QCheck.Gen.t = QCheck.Gen.frequency api
+  let gen_cmd gen_t_var : ('a option * cmd) QCheck.Gen.t = QCheck.Gen.frequency (api gen_t_var)
 
   let show_cmd (Cmd { args ; print ; _ }) = print args
 
-  let shrink_cmd (Cmd cmd) =
-    QCheck.Iter.map (fun args -> Cmd { cmd with args }) (cmd.shrink cmd.args)
+  let rec args_use_var
+    : type a r. Internal.Var.t -> (a, r) Args.args -> bool =
+    fun var args ->
+    match args with
+    | FnState (i, args') -> i=var || args_use_var var args'
+    | Fn (_, args')      -> args_use_var var args'
+    | _                  -> false
+
+  let cmd_uses_var var (Cmd { args; _ }) = args_use_var var args
+
+  let rec shrink_t_vars
+    : type a r. Internal.Env.t -> (a, r) Args.args -> (a, r) Args.args QCheck.Iter.t =
+    fun env args ->
+    match args with
+    | FnState (i,args') ->
+      QCheck.Iter.(map (fun i -> Args.FnState (i,args')) (Internal.Env.valid_t_vars env i)
+                   <+>
+                   map (fun args' -> Args.FnState (i, args')) (shrink_t_vars env args'))
+    | Fn (a,args') -> QCheck.Iter.map (fun args' -> Args.Fn (a, args')) (shrink_t_vars env args')
+    | _            -> QCheck.Iter.empty
+
+  let shrink_cmd (env : Internal.Env.t) (Cmd cmd) =
+    QCheck.Iter.( (* reduce t-vars first as it can trigger removal of other cmds *)
+      map (fun args -> Cmd { cmd with args }) (shrink_t_vars env cmd.args)
+      <+> (* only secondly reduce char/int/... arguments *)
+      map (fun args -> Cmd { cmd with args }) (cmd.shrink cmd.args)
+    )
 
   (* Unsafe if called on two [res] whose internal values are of different
      types. *)
@@ -413,7 +564,7 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
     | GenDeconstr (_, print, _) -> print value
 
   let rec apply_f
-    : type a r. a -> (a, r) Args.args -> t -> r = fun f args state ->
+    : type a r. a -> (a, r) Args.args -> t array -> Internal.Var.t option -> r = fun f args state opt_target ->
     match args with
     | Ret _ ->
       f
@@ -425,24 +576,31 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
     | Ret_ignore_or_exc _ ->
       (* A constant value in the API cannot raise an exception *)
       raise (Invalid_argument "apply_f")
-    | FnState (Ret _) ->
-      f state
-    | FnState (Ret_or_exc _) ->
-      begin
-        try Ok (f state)
-        with e -> Error e
-      end
-    | FnState (Ret_ignore _) ->
-      ignore (f state)
-    | FnState (Ret_ignore_or_exc _) ->
-      begin
-        try Ok (ignore @@ f state)
-        with e -> Error e
-      end
-    | FnState (Fn _ as rem) ->
-      apply_f (f state) rem state
-    | FnState (FnState _ as rem) ->
-      apply_f (f state) rem state
+    | FnState (index, Ret _) ->
+        f state.(index)
+    | FnState (index, Ret_or_exc _) ->
+        begin
+          try Ok (f state.(index))
+          with e -> Error e
+        end
+    | FnState (index, Ret_ignore ty) ->
+      (match ty,opt_target with
+       | State, Some tgt -> state.(tgt) <- (f state.(index))
+       | _               -> ignore (f state.(index)))
+    | FnState (index, Ret_ignore_or_exc ty) ->
+      (match ty,opt_target with
+       | State, Some tgt ->
+         begin
+           try Ok (state.(tgt) <- f state.(index))
+           with e -> Error e
+         end
+       | _ ->
+         begin
+           try Ok (ignore @@ f state.(index))
+           with e -> Error e
+         end)
+    | FnState (index, rem) ->
+        apply_f (f state.(index)) rem state opt_target
     | Fn (arg, Ret _) ->
       f arg
     | Fn (arg, Ret_or_exc _) ->
@@ -457,12 +615,10 @@ module MakeCmd (ApiSpec : Spec) : Internal.CmdSpec = struct
         try Ok (ignore @@ f arg)
         with e -> Error e
       end
-    | Fn (arg, (Fn _ as rem)) ->
-      apply_f (f arg) rem state
-    | Fn (arg, (FnState _ as rem)) ->
-      apply_f (f arg) rem state
+    | Fn (arg, rem) ->
+      apply_f (f arg) rem state opt_target
 
-  let run cmd state =
+  let run (opt_target,cmd) state =
     let Cmd { args ; rty ; f ; _ } = cmd in
-    Res (rty, apply_f f args state)
+    Res (rty, apply_f f args state opt_target)
 end
diff --git a/lib/lin.mli b/lib/lin.mli
index 29c849b87..25ea8d12a 100644
--- a/lib/lin.mli
+++ b/lib/lin.mli
@@ -7,6 +7,20 @@
     at any time.
  *)
 module Internal : sig
+  module Var : sig
+    type t = int
+    val next : unit -> t
+    val reset : unit -> unit
+    val pp : Format.formatter -> t -> unit
+    val show : t -> string
+  end
+
+  module Env : sig
+    type t = Var.t list
+    val gen_t_var : t -> Var.t QCheck.Gen.t
+    val valid_t_vars : t -> Var.t -> Var.t QCheck.Iter.t
+  end
+
   module type CmdSpec = sig
     type t
     (** The type of the system under test *)
@@ -17,12 +31,18 @@ module Internal : sig
     val show_cmd : cmd -> string
     (** [show_cmd c] returns a string representing the command [c]. *)
 
-    val gen_cmd : cmd QCheck.Gen.t
-    (** A command generator. *)
+    val gen_cmd : Var.t QCheck.Gen.t -> (Var.t option * cmd) QCheck.Gen.t
+    (** A command generator.
+        It accepts a variable generator and generates a pair [(opt,cmd)] with the option indicating
+        an storage index to store the [cmd]'s result. *)
 
-    val shrink_cmd : cmd QCheck.Shrink.t
+    val shrink_cmd : Env.t -> cmd QCheck.Shrink.t
     (** A command shrinker.
-        To a first approximation you can use {!QCheck.Shrink.nil}. *)
+        It accepts the current environment as its argument.
+        To a first approximation you can use [fun _env -> Shrink.nil]. *)
+
+    val cmd_uses_var : Var.t -> cmd -> bool
+    (** [cmd_uses_var v cmd] should return [true] iff the command [cmd] refers to the variable [v]. *)
 
     type res
     (** The command result type *)
@@ -40,16 +60,27 @@ module Internal : sig
     (** Utility function to clean up [t] after each test instance,
         e.g., for closing sockets, files, or resetting global parameters *)
 
-    val run : cmd -> t -> res
-    (** [run c t] should interpret the command [c] over the system under test [t] (typically side-effecting). *)
+    val run : (Var.t option * cmd) -> t array -> res
+    (** [run (opt,c) t] should interpret the command [c] over the various instances of the system under test [t array] (typically side-effecting).
+        [opt] indicates the index to store the result. *)
   end
 
+  type 'cmd cmd_triple =
+    { env_size   : int;
+      seq_prefix : (Var.t option * 'cmd) list;
+      tail_left  : (Var.t option * 'cmd) list;
+      tail_right : (Var.t option * 'cmd) list; }
+
   module Make(Spec : CmdSpec) : sig
-    val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
-    val check_seq_cons : (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> Spec.t -> Spec.cmd list -> bool
-    val interp_plain : Spec.t -> Spec.cmd list -> (Spec.cmd * Spec.res) list
-    val lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t
-    val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd list * Spec.cmd list * Spec.cmd list -> bool) -> QCheck.Test.t
+    val init_sut : int -> Spec.t array
+    val cleanup : Spec.t array -> (Var.t option * Spec.cmd) list -> (Var.t option * Spec.cmd) list -> (Var.t option * Spec.cmd) list -> unit
+    val show_cmd : Var.t option * Spec.cmd -> string
+    val init_cmd_ret : string
+    val arb_cmds_triple : int -> int -> Spec.cmd cmd_triple QCheck.arbitrary
+    val check_seq_cons : int -> ((Var.t option * Spec.cmd) * Spec.res) list -> ((Var.t option * Spec.cmd) * Spec.res) list -> ((Var.t option * Spec.cmd) * Spec.res) list -> Spec.t array -> (Var.t option * Spec.cmd) list -> bool
+    val interp_plain : Spec.t array -> (Var.t option * Spec.cmd) list -> ((Var.t option * Spec.cmd) * Spec.res) list
+    val lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd cmd_triple -> bool) -> QCheck.Test.t
+    val neg_lin_test : rep_count:int -> retries:int -> count:int -> name:string -> lin_prop:(Spec.cmd cmd_triple -> bool) -> QCheck.Test.t
   end
 
   val pp_exn : Format.formatter -> exn -> unit
@@ -200,6 +231,12 @@ val array : ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty
     and have their elements generated by the [t] combinator.
     It is based on {!QCheck.array}. *)
 
+val bounded_array : int -> ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty
+(** The [bounded_array] combinator represents the {{!Stdlib.Array.t}[array]} type.
+    The generated arrays from [bounded_array len t] have a length between [0] and [len]
+    (inclusive) and have their elements generated by the [t] combinator.
+    It is based on {!QCheck.array_of_size}. *)
+
 val seq : ('a, 'c, 's, combinable) ty -> ('a Seq.t, 'c, 's, combinable) ty
 (** The [seq] combinator represents the {!Stdlib.Seq.t} type.
     The generated sequences from [seq t] have a length resulting from {!QCheck.Gen.nat}
diff --git a/lib/lin_domain.ml b/lib/lin_domain.ml
index 4c525e673..8c025d6c8 100644
--- a/lib/lin_domain.ml
+++ b/lib/lin_domain.ml
@@ -11,23 +11,23 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
     List.combine cs (Array.to_list res_arr)
 
   (* Linearization property based on [Domain] and an Atomic flag *)
-  let lin_prop (seq_pref,cmds1,cmds2) =
-    let sut = Spec.init () in
+  let lin_prop { Internal.env_size=array_size; seq_prefix=seq_pref; tail_left=cmds1; tail_right=cmds2 } =
+    let sut = init_sut array_size in
     let pref_obs = interp sut seq_pref in
     let wait = Atomic.make true in
     let dom1 = Domain.spawn (fun () -> while Atomic.get wait do Domain.cpu_relax() done; try Ok (interp sut cmds1) with exn -> Error exn) in
     let dom2 = Domain.spawn (fun () -> Atomic.set wait false; try Ok (interp sut cmds2) with exn -> Error exn) in
     let obs1 = Domain.join dom1 in
     let obs2 = Domain.join dom2 in
-    Spec.cleanup sut ;
+    cleanup sut seq_pref cmds1 cmds2;
     let obs1 = match obs1 with Ok v -> v | Error exn -> raise exn in
     let obs2 = match obs2 with Ok v -> v | Error exn -> raise exn in
-    let seq_sut = Spec.init () in
-    check_seq_cons pref_obs obs1 obs2 seq_sut []
+    let seq_sut = init_sut array_size in
+    check_seq_cons array_size pref_obs obs1 obs2 seq_sut []
       || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
-         @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
-              (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
-              (pref_obs,obs1,obs2)
+         @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd:init_cmd_ret
+              (fun (c,r) -> Printf.sprintf "%s : %s" (show_cmd c) (Spec.show_res r))
+              (pref_obs,obs1,obs2)[@@alert "-internal"]
 
   let lin_test ~count ~name =
     lin_test ~rep_count:50 ~count ~retries:3 ~name ~lin_prop:lin_prop
diff --git a/lib/lin_domain.mli b/lib/lin_domain.mli
index f8306a442..50aeada9d 100644
--- a/lib/lin_domain.mli
+++ b/lib/lin_domain.mli
@@ -2,8 +2,9 @@ open Lin
 
 (** functor to build an internal module representing parallel tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
-  val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
-  val lin_prop : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
+  [@@@alert "-internal"]
+  val arb_cmds_triple : int -> int -> Spec.cmd Internal.cmd_triple QCheck.arbitrary
+  val lin_prop : Spec.cmd Internal.cmd_triple -> bool
   val lin_test : count:int -> name:string -> QCheck.Test.t
   val neg_lin_test : count:int -> name:string -> QCheck.Test.t
 end
diff --git a/lib/lin_effect.ml b/lib/lin_effect.ml
index 0a123a47c..24973d2bf 100644
--- a/lib/lin_effect.ml
+++ b/lib/lin_effect.ml
@@ -51,14 +51,18 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       | SchedYield -> "<SchedYield>"
       | UserCmd c  -> Spec.show_cmd c
 
-    let gen_cmd =
+    let gen_cmd env =
       (Gen.frequency
-         [(3,Gen.return SchedYield);
-          (5,Gen.map (fun c -> UserCmd c) Spec.gen_cmd)])
+         [(3,Gen.return (None,SchedYield));
+          (5,Gen.map (fun (opt,c) -> (opt,UserCmd c)) (Spec.gen_cmd env))])
 
-    let shrink_cmd c = match c with
+    let shrink_cmd env c = match c with
       | SchedYield -> Iter.empty
-      | UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd c)
+      | UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd env c)
+
+    let cmd_uses_var var c = match c with
+      | SchedYield -> false
+      | UserCmd cmd -> Spec.cmd_uses_var var cmd
 
     type res = SchedYieldRes | UserRes of Spec.res
 
@@ -72,10 +76,10 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
       | _, _ -> false
 
     let run c sut = match c with
-      | SchedYield ->
+      | _, SchedYield ->
           (yield (); SchedYieldRes)
-      | UserCmd uc ->
-          let res = Spec.run uc sut in
+      | opt, UserCmd uc ->
+          let res = Spec.run (opt,uc) sut in
           UserRes res
   end
 
@@ -83,7 +87,7 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
 
   let arb_cmds_triple = EffTest.arb_cmds_triple
 
-  let filter_res rs = List.filter (fun (c,_) -> c <> EffSpec.SchedYield) rs
+  let filter_res rs = List.filter (fun ((_,c),_) -> c <> EffSpec.SchedYield) rs
 
   let rec interp sut cs = match cs with
     | [] -> []
@@ -92,25 +96,25 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
         (c,res)::interp sut cs
 
   (* Concurrent agreement property based on effect-handler scheduler *)
-  let lin_prop (seq_pref,cmds1,cmds2) =
-    let sut = Spec.init () in
+  let lin_prop { Internal.env_size=array_size; seq_prefix=seq_pref; tail_left=cmds1; tail_right=cmds2 } =
+    let sut = EffTest.init_sut array_size in
+    let pref_obs = EffTest.interp_plain sut (List.filter (fun (_,c) -> c <> EffSpec.SchedYield) seq_pref) in
     (* exclude [Yield]s from sequential prefix *)
-    let pref_obs = EffTest.interp_plain sut (List.filter (fun c -> c <> EffSpec.SchedYield) seq_pref) in
     let obs1,obs2 = ref (Ok []), ref (Ok []) in
     let main () =
       fork (fun () -> let tmp1 = try Ok (interp sut cmds1) with exn -> Error exn in obs1 := tmp1);
       fork (fun () -> let tmp2 = try Ok (interp sut cmds2) with exn -> Error exn in obs2 := tmp2); in
     let () = start_sched main in
-    let () = Spec.cleanup sut in
+    let () = EffTest.cleanup sut seq_pref cmds1 cmds2 in
     let obs1 = match !obs1 with Ok v -> ref v | Error exn -> raise exn in
     let obs2 = match !obs2 with Ok v -> ref v | Error exn -> raise exn in
-    let seq_sut = Spec.init () in
+    let seq_sut = EffTest.init_sut array_size in
     (* exclude [Yield]s from sequential executions when searching for an interleaving *)
-    EffTest.check_seq_cons (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut []
+    EffTest.check_seq_cons array_size (filter_res pref_obs) (filter_res !obs1) (filter_res !obs2) seq_sut []
     || QCheck.Test.fail_reportf "  Results incompatible with linearized model\n\n%s"
-    @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
-      (fun (c,r) -> Printf.sprintf "%s : %s" (EffSpec.show_cmd c) (EffSpec.show_res r))
-      (pref_obs,!obs1,!obs2)
+    @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd:EffTest.init_cmd_ret
+      (fun (c,r) -> Printf.sprintf "%s : %s" (EffTest.show_cmd c) (EffSpec.show_res r))
+      (pref_obs,!obs1,!obs2)[@@alert "-internal"]
 
   let lin_test ~count ~name =
     let arb_cmd_triple = EffTest.arb_cmds_triple 20 12 in
diff --git a/lib/lin_effect.mli b/lib/lin_effect.mli
index 0885c18ec..453e370db 100644
--- a/lib/lin_effect.mli
+++ b/lib/lin_effect.mli
@@ -5,8 +5,9 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
   module EffSpec : sig
     type cmd
   end
-  val arb_cmds_triple : int -> int -> (EffSpec.cmd list * EffSpec.cmd list * EffSpec.cmd list) QCheck.arbitrary
-  val lin_prop : (EffSpec.cmd list * EffSpec.cmd list * EffSpec.cmd list) -> bool
+  [@@@alert "-internal"]
+  val arb_cmds_triple : int -> int -> EffSpec.cmd Internal.cmd_triple QCheck.arbitrary
+  val lin_prop : EffSpec.cmd Internal.cmd_triple -> bool
   val lin_test : count:int -> name:string -> QCheck.Test.t
   val neg_lin_test : count:int -> name:string -> QCheck.Test.t
 end
diff --git a/lib/lin_thread.ml b/lib/lin_thread.ml
index 2b8658cb0..e3d418928 100644
--- a/lib/lin_thread.ml
+++ b/lib/lin_thread.ml
@@ -18,8 +18,8 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
   let arb_cmds_triple = arb_cmds_triple
 
   (* Linearization property based on [Thread] *)
-  let lin_prop (seq_pref, cmds1, cmds2) =
-    let sut = Spec.init () in
+  let lin_prop { Internal.env_size=array_size; seq_prefix=seq_pref; tail_left=cmds1; tail_right=cmds2 } =
+    let sut = init_sut array_size in
     let obs1, obs2 = ref (Ok []), ref (Ok []) in
     let pref_obs = interp_plain sut seq_pref in
     let wait = ref true in
@@ -27,16 +27,16 @@ module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) = struct
     let th2 = Thread.create (fun () -> wait := false; obs2 := try Ok (interp_thread sut cmds2) with exn -> Error exn) () in
     Thread.join th1;
     Thread.join th2;
-    Spec.cleanup sut;
+    cleanup sut seq_pref cmds1 cmds2;
     let obs1 = match !obs1 with Ok v -> ref v | Error exn -> raise exn in
     let obs2 = match !obs2 with Ok v -> ref v | Error exn -> raise exn in
-    let seq_sut = Spec.init () in
+    let seq_sut = init_sut array_size in
     (* we reuse [check_seq_cons] to linearize and interpret sequentially *)
-    check_seq_cons pref_obs !obs1 !obs2 seq_sut []
+    check_seq_cons array_size pref_obs !obs1 !obs2 seq_sut []
     || QCheck.Test.fail_reportf "  Results incompatible with sequential execution\n\n%s"
-       @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35
-            (fun (c,r) -> Printf.sprintf "%s : %s" (Spec.show_cmd c) (Spec.show_res r))
-            (pref_obs,!obs1,!obs2)
+       @@ Util.print_triple_vertical ~fig_indent:5 ~res_width:35 ~init_cmd:init_cmd_ret
+            (fun (c,r) -> Printf.sprintf "%s : %s" (show_cmd c) (Spec.show_res r))
+            (pref_obs,!obs1,!obs2)[@@alert "-internal"]
 
   let lin_test ~count ~name =
     lin_test ~rep_count:100 ~count ~retries:5 ~name ~lin_prop:lin_prop
diff --git a/lib/lin_thread.mli b/lib/lin_thread.mli
index bae14a5eb..abbcba5c7 100644
--- a/lib/lin_thread.mli
+++ b/lib/lin_thread.mli
@@ -2,8 +2,9 @@ open Lin
 
 (** functor to build an internal module representing concurrent tests *)
 module Make_internal (Spec : Internal.CmdSpec [@alert "-internal"]) : sig
-  val arb_cmds_triple : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) QCheck.arbitrary
-  val lin_prop : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
+  [@@@alert "-internal"]
+  val arb_cmds_triple : int -> int -> Spec.cmd Internal.cmd_triple QCheck.arbitrary
+  val lin_prop : Spec.cmd Internal.cmd_triple -> bool
   val lin_test : count:int -> name:string -> QCheck.Test.t
   val neg_lin_test : count:int -> name:string -> QCheck.Test.t
 end
diff --git a/lib/util.ml b/lib/util.ml
index be23eedf8..6e0249180 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -37,8 +37,9 @@ let print_vertical ?(fig_indent=3) show cmds =
   let () = List.iter (fun c -> indent (); print_seq_col c) cmds in
   Buffer.contents buf
 
-let print_triple_vertical ?(fig_indent=10) ?(res_width=20) ?(center_prefix=true) show (seq,cmds1,cmds2) =
+let print_triple_vertical ?(fig_indent=10) ?(res_width=20) ?(center_prefix=true) ?init_cmd show (seq,cmds1,cmds2) =
   let seq,cmds1,cmds2 = List.(map show seq, map show cmds1, map show cmds2) in
+  let seq = match init_cmd with None -> seq | Some init_cmd -> init_cmd::seq in
   let max_width ss = List.fold_left max 0 (List.map String.length ss) in
   let width = List.fold_left max 0 [max_width seq; max_width cmds1; max_width cmds2] in
   let res_width = max width res_width in
diff --git a/lib/util.mli b/lib/util.mli
index 915458017..7bbee96cb 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -29,6 +29,7 @@ val print_triple_vertical :
   ?fig_indent:int ->
   ?res_width:int ->
   ?center_prefix:bool ->
+  ?init_cmd:string ->
   ('a -> string) -> 'a list * 'a list * 'a list -> string
 (** [print_triple_vertical pr (xs,ys,zs)] returns a string representing a
     parallel trace, with [xs] printed first, and then [ys] and [zs] printed
@@ -36,6 +37,7 @@ val print_triple_vertical :
     Optional [fig_indent] indicates how many spaces it should be indented (default: 10 spaces).
     Optional [res_width] specifies the reserved width for printing each list entry (default: 20 chars).
     Optional [center_prefix] centers the sequential prefix if [true] (the default) and otherwise left-adjust it.
+    Optional [init_cmd] indicates a string-rendered, initial command.
  *)
 
 val protect : ('a -> 'b) -> 'a -> ('b, exn) result
diff --git a/src/array/lin_tests.ml b/src/array/lin_tests.ml
index ee935fd3f..c4af7cdfd 100644
--- a/src/array/lin_tests.ml
+++ b/src/array/lin_tests.ml
@@ -7,30 +7,82 @@ module AConf =
 struct
   type t = char array
 
+ (* note to self:
+    - generate one t_var per input [t] parameter and
+    - record [Env.next] for each resulting [t] in an option *)
+  open Lin
+  open Internal [@@alert "-internal"]
   type cmd =
-    | Length
-    | Get of int'
-    | Set of int' * char'
-    | Sub of int' * int'
-    | Copy
-    | Fill of int' * int' * char'
-    | To_list
-    | Mem of char'
-    | Sort
-    | To_seq [@@deriving qcheck, show { with_path = false }]
-  and int' = int [@gen Gen.small_nat]
-  and char' = char [@gen Gen.printable]
-
-  let shrink_cmd c = Iter.empty
+    | Length of Var.t
+    | Get of Var.t * int
+    | Set of Var.t * int * char
+    | Append of Var.t * Var.t
+    | Sub of Var.t * int * int
+    | Copy of Var.t
+    | Fill of Var.t * int * int * char
+    | To_list of Var.t
+    | Mem of Var.t * char
+    | Sort of Var.t
+    | To_seq of Var.t [@@deriving show { with_path = false }]
+
+  let gen_int = Gen.small_nat
+  let gen_char = Gen.printable
+  let map4 f w x y z st = f (w st) (x st) (y st) (z st)
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun t -> (None, Length t)) gen_var;
+        map2 (fun t i -> (None, Get (t,i))) gen_var gen_int;
+        map3 (fun t i c -> (None, Set (t,i,c))) gen_var gen_int gen_char;
+        map2 (fun t1 t2 -> (Some (Var.next ()), Append (t1,t2))) gen_var gen_var;
+        map3 (fun v i l -> (Some (Var.next ()), Sub (v,i,l))) gen_var gen_int gen_int;
+        map  (fun t -> (Some (Var.next ()), Copy t)) gen_var;
+        map4 (fun v i l c -> (None, Fill (v,i,l,c))) gen_var gen_int gen_int gen_char;
+        map  (fun v -> (None, To_list v)) gen_var;
+        map2 (fun v c -> (None, Mem (v,c))) gen_var gen_char;
+        map  (fun v -> (None, Sort v)) gen_var;
+        map  (fun v -> (None, To_seq v)) gen_var;
+      ])
+
+  let shrink_cmd env c = match c with
+    | Length v     -> Iter.map (fun v -> Length v)    (Env.valid_t_vars env v)
+    | Get (v,i)    -> Iter.map (fun v -> Get (v,i))   (Env.valid_t_vars env v)
+    | Set (v,i,c)  -> Iter.map (fun v -> Set (v,i,c)) (Env.valid_t_vars env v)
+    | Append (v,w) ->
+      Iter.(map (fun v -> Append (v,w)) (Env.valid_t_vars env v)
+            <+>
+            map (fun w -> Append (v,w)) (Env.valid_t_vars env w))
+    | Sub (v,i,l) -> Iter.map (fun v -> Sub (v,i,l)) (Env.valid_t_vars env v)
+    | Copy v      -> Iter.map (fun v -> Copy v)      (Env.valid_t_vars env v)
+    | Fill (v,i,l,c) -> Iter.map (fun v -> Fill (v,i,l,c)) (Env.valid_t_vars env v)
+    | To_list v   -> Iter.map (fun v -> To_list v)   (Env.valid_t_vars env v)
+    | Mem (v,c)   -> Iter.map (fun v -> Mem (v,c))   (Env.valid_t_vars env v)
+    | Sort v      -> Iter.map (fun v -> Sort v)      (Env.valid_t_vars env v)
+    | To_seq v    -> Iter.map (fun v -> To_seq v)    (Env.valid_t_vars env v)
+
+  let cmd_uses_var v c = match c with
+    | Length i
+    | Get (i,_)
+    | Set (i,_,_)
+    | Sub (i,_,_)
+    | Copy i
+    | Fill (i,_,_,_)
+    | To_list i
+    | Mem (i,_)
+    | Sort i
+    | To_seq i -> i=v
+    | Append (i,j) -> i=v || j=v
 
   open Util
   (*let pp_exn = Util.pp_exn*)
+  (*let pp fmt t = Format.fprintf fmt "%s" (QCheck.Print.(array char) t)
+    let equal a1 a2 = Array.for_all2 (=) a1 a2*)
   type res =
     | RLength of int
     | RGet of ((char, exn) result)
     | RSet of ((unit, exn) result)
-    | RSub of ((char array, exn) result)
-    | RCopy of char array
+    | RAppend of unit
+    | RSub of ((unit, exn) result)
+    | RCopy of unit
     | RFill of ((unit, exn) result)
     | RTo_list of char list
     | RMem of bool
@@ -38,21 +90,27 @@ struct
     | RTo_seq of (char Seq.t [@printer fun fmt seq -> fprintf fmt "%s" (QCheck.Print.(list char) (List.of_seq seq))])
   [@@deriving show { with_path = false }, eq]
 
-  let array_size = 16
+  let array_size = 2
 
   let init () = Array.make array_size 'a'
 
+  (* FIXME:
+     - shrink target variables generically:
+       match on optional target i, unless someone is refering to it (how to tell for arb. cmds?)
+  *)
   let run c a = match c with
-    | Length        -> RLength (Array.length a)
-    | Get i         -> RGet (Util.protect (Array.get a) i)
-    | Set (i,c)     -> RSet (Util.protect (Array.set a i) c)
-    | Sub (i,l)     -> RSub (Util.protect (Array.sub a i) l)
-    | Copy          -> RCopy (Array.copy a)
-    | Fill (i,l,c)  -> RFill (Util.protect (Array.fill a i l) c)
-    | To_list       -> RTo_list (Array.to_list a)
-    | Mem c         -> RMem (Array.mem c a)
-    | Sort          -> RSort (Array.sort Char.compare a)
-    | To_seq        -> RTo_seq (List.to_seq (List.of_seq (Array.to_seq a))) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *)
+    | None,   Length v       -> RLength (Array.length a.(v))
+    | None,   Get (v,i)      -> RGet (Util.protect (Array.get a.(v)) i)
+    | None,   Set (v,i,c)    -> RSet (Util.protect (Array.set a.(v) i) c)
+    | Some r, Append (v,w)   -> RAppend (let tmp = Array.append a.(v) a.(w) in a.(r) <- tmp)
+    | Some r, Sub (v,i,l)    -> RSub (Util.protect (fun () -> let tmp = Array.sub a.(v) i l in a.(r) <- tmp) ())
+    | Some r, Copy v         -> RCopy (let tmp = Array.copy a.(v) in a.(r) <- tmp)
+    | None,   Fill (v,i,l,c) -> RFill (Util.protect (Array.fill a.(v) i l) c)
+    | None,   To_list v      -> RTo_list (Array.to_list a.(v))
+    | None,   Mem (v,c)      -> RMem (Array.mem c a.(v))
+    | None,   Sort v         -> RSort (Array.sort Char.compare a.(v))
+    | None,   To_seq v       -> RTo_seq (List.to_seq (List.of_seq (Array.to_seq a.(v)))) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
   let cleanup _ = ()
 end
 
diff --git a/src/array/lin_tests_dsl.ml b/src/array/lin_tests_dsl.ml
index fb5b67f27..d0165104f 100644
--- a/src/array/lin_tests_dsl.ml
+++ b/src/array/lin_tests_dsl.ml
@@ -5,7 +5,7 @@ module AConf =
 struct
   type t = char array
 
-  let array_size = 16
+  let array_size = 2
   let init () = Array.make array_size 'a'
   let cleanup _ = ()
 
@@ -16,10 +16,13 @@ struct
     [ val_ "Array.length"   Array.length   (t @-> returning int);
       val_ "Array.get"      Array.get      (t @-> int @-> returning_or_exc char);
       val_ "Array.set"      Array.set      (t @-> int @-> char @-> returning_or_exc unit);
-      val_ "Array.sub"      Array.sub      (t @-> int @-> int @-> returning_or_exc (array char));
-      val_ "Array.copy"     Array.copy     (t @-> returning (array char));
+      val_ "Array.append"   Array.append   (t @-> t @-> returning_ t);
+      val_ "Array.sub"      Array.sub      (t @-> int @-> int @-> returning_or_exc_ t);
+      val_ "Array.copy"     Array.copy     (t @-> returning_ t);
       val_ "Array.fill"     Array.fill     (t @-> int @-> int @-> char @-> returning_or_exc unit);
+      val_ "Array.blit"     Array.blit     (t @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
       val_ "Array.to_list"  Array.to_list  (t @-> returning (list char));
+      val_ "Array.of_list"  Array.of_list  (list char @-> returning_ t);
       val_ "Array.mem"      Array.mem      (char @-> t @-> returning bool);
       val_ "Array.sort"     (Array.sort Char.compare) (t @-> returning unit);
       val_ "Array.to_seq"   array_to_seq   (t @-> returning (seq char));
diff --git a/src/atomic/lin_tests.ml b/src/atomic/lin_tests.ml
index 5c63eafd4..1107c4f67 100644
--- a/src/atomic/lin_tests.ml
+++ b/src/atomic/lin_tests.ml
@@ -6,44 +6,71 @@ open QCheck
 module AConf =
 struct
   type t = int Atomic.t
-
+  open Lin
+  open Internal [@@alert "-internal"]
   type cmd =
-    | Get
-    | Set of int'
-    | Exchange of int'
-    | Compare_and_set of int' * int'
-    | Fetch_and_add of int'
-    | Incr
-    | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = int [@gen Gen.nat]
-
-  let shrink_cmd = Shrink.nil
+    | Make of int
+    | Get of Var.t
+    | Set of Var.t * int
+    | Exchange of Var.t * int
+    | Compare_and_set of Var.t * int * int
+    | Fetch_and_add of Var.t * int
+    | Incr of Var.t
+    | Decr of Var.t [@@deriving show { with_path = false }]
+
+  let gen_int = Gen.nat
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun i ->     (Some (Var.next()), Make i)) gen_int;
+        map  (fun t ->     (None, Get t)) gen_var;
+        map2 (fun t i ->   (None, Set (t,i))) gen_var gen_int;
+        map2 (fun t i ->   (None, Exchange (t,i))) gen_var gen_int;
+        map3 (fun t i j -> (None, Compare_and_set (t,i,j))) gen_var gen_int gen_int;
+        map2 (fun t i ->   (None, Fetch_and_add (t,i))) gen_var gen_int;
+        map  (fun t ->     (None, Incr t)) gen_var;
+        map  (fun t ->     (None, Decr t)) gen_var;
+      ])
+
+  let shrink_cmd _env = Shrink.nil
+
+  let cmd_uses_var v = function
+    | Make _ -> false
+    | Get i
+    | Set (i,_)
+    | Exchange (i,_)
+    | Compare_and_set (i,_,_)
+    | Fetch_and_add (i,_)
+    | Incr i
+    | Decr i -> i=v
 
   type res =
+    | RMake of unit
     | RGet of int
-    | RSet
+    | RSet of unit
     | RExchange of int
     | RFetch_and_add of int
     | RCompare_and_set of bool
-    | RIncr
-    | RDecr [@@deriving show { with_path = false }, eq]
+    | RIncr of unit
+    | RDecr of unit [@@deriving show { with_path = false }, eq]
 
   let init () = Atomic.make 0
 
   let run c r = match c with
-    | Get                      -> RGet (Atomic.get r)
-    | Set i                    -> (Atomic.set r i; RSet)
-    | Exchange i               -> RExchange (Atomic.exchange r i)
-    | Fetch_and_add i          -> RFetch_and_add (Atomic.fetch_and_add r i)
-    | Compare_and_set (seen,v) -> RCompare_and_set (Atomic.compare_and_set r seen v)
-    | Incr                     -> (Atomic.incr r; RIncr)
-    | Decr                     -> (Atomic.decr r; RDecr)
+    | Some t, Make i                   -> RMake (r.(t) <- Atomic.make i)
+    | None, Get t                      -> RGet (Atomic.get r.(t))
+    | None, Set (t,i)                  -> RSet (Atomic.set r.(t) i)
+    | None, Exchange (t,i)             -> RExchange (Atomic.exchange r.(t) i)
+    | None, Fetch_and_add (t,i)        -> RFetch_and_add (Atomic.fetch_and_add r.(t) i)
+    | None, Compare_and_set (t,seen,v) -> RCompare_and_set (Atomic.compare_and_set r.(t) seen v)
+    | None, Incr t                     -> RIncr (Atomic.incr r.(t))
+    | None, Decr t                     -> RDecr (Atomic.decr r.(t))
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end
 
 module AT_domain = Lin_domain.Make_internal(AConf) [@alert "-internal"]
-
+(*
 (** A variant of the above with 3 Atomics *)
 module A3Conf =
 struct
@@ -84,10 +111,10 @@ struct
 
   let cleanup _ = ()
 end
-
-module A3T_domain = Lin_domain.Make_internal(A3Conf) [@alert "-internal"]
+*)
+(*module A3T_domain = Lin_domain.Make_internal(A3Conf) [@alert "-internal"]*)
 ;;
 QCheck_base_runner.run_tests_main [
   AT_domain.lin_test  ~count:1000 ~name:"Lin Atomic test with Domain";
-  A3T_domain.lin_test ~count:1000 ~name:"Lin Atomic3 test with Domain";
+  (*A3T_domain.lin_test ~count:1000 ~name:"Lin Atomic3 test with Domain";*)
 ]
diff --git a/src/atomic/lin_tests_dsl.ml b/src/atomic/lin_tests_dsl.ml
index 88e7c2e38..2b92a92f0 100644
--- a/src/atomic/lin_tests_dsl.ml
+++ b/src/atomic/lin_tests_dsl.ml
@@ -3,8 +3,10 @@ module Atomic_spec : Lin.Spec = struct
   type t = int Atomic.t
   let init () = Atomic.make 0
   let cleanup _ = ()
+  let int = int_small
   let api =
-    [ val_ "Atomic.get"             Atomic.get             (t @-> returning int);
+    [ val_ "Atomic.make"            Atomic.make            (int @-> returning_ t);
+      val_ "Atomic.get"             Atomic.get             (t @-> returning int);
       val_ "Atomic.set"             Atomic.set             (t @-> int @-> returning unit);
       val_ "Atomic.exchange"        Atomic.exchange        (t @-> int @-> returning int);
       val_ "Atomic.fetch_and_add"   Atomic.fetch_and_add   (t @-> int @-> returning int);
diff --git a/src/bigarray/lin_tests_dsl.ml b/src/bigarray/lin_tests_dsl.ml
index fbd609ed9..7103de980 100644
--- a/src/bigarray/lin_tests_dsl.ml
+++ b/src/bigarray/lin_tests_dsl.ml
@@ -2,26 +2,62 @@
 (*           Tests of thread-unsafe [Bigarray.Array1] of ints             *)
 (* ********************************************************************** *)
 
+(* Bigarray.Array1 API:
+
+    val create : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> int -> ('a, 'b, 'c) t
+    val init : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> int -> (int -> 'a) -> ('a, 'b, 'c) t
+    external dim : ('a, 'b, 'c) t -> int
+    external kind : ('a, 'b, 'c) t -> ('a, 'b) Bigarray.kind
+    external layout : ('a, 'b, 'c) t -> 'c Bigarray.layout
+    val change_layout : ('a, 'b, 'c) t -> 'd Bigarray.layout -> ('a, 'b, 'd) t
+    val size_in_bytes : ('a, 'b, 'c) t -> int
+    external get : ('a, 'b, 'c) t -> int -> 'a
+    external set : ('a, 'b, 'c) t -> int -> 'a -> unit
+    external sub : ('a, 'b, 'c) t -> int -> int -> ('a, 'b, 'c) t
+    val slice : ('a, 'b, 'c) t -> int -> ('a, 'b, 'c) Bigarray.Array0.t
+    external blit : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> unit
+    external fill : ('a, 'b, 'c) t -> 'a -> unit
+    val of_array : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> 'a array -> ('a, 'b, 'c) t
+    external unsafe_get : ('a, 'b, 'c) t -> int -> 'a
+    external unsafe_set : ('a, 'b, 'c) t -> int -> 'a -> unit
+*)
+
 module BA1Conf =
 struct
   open Bigarray
   type t = (int, int_elt, c_layout) Array1.t
 
-  let array_size = 16
-  let init () =
-    let arr = Array1.create int C_layout array_size in
+  let array_create sz =
+    let arr = Array1.create int C_layout sz in
     Array1.fill arr 0 ;
     arr
+  let of_array = Array1.of_array int C_layout
+  let dummy_change_layout arr = Array1.change_layout arr C_layout
+
+  let array_size = 16
+  let init () = array_create array_size
   let cleanup _ = ()
 
   open Lin
   let int = int_small
 
   let api =
-    [ val_ "Bigarray.Array1.size_in_bytes" Array1.size_in_bytes (t @-> returning int);
-      val_ "Bigarray.Array1.get"           Array1.get           (t @-> int @-> returning_or_exc int);
+    [ val_ "Bigarray.Array1.create"        array_create         (int @-> returning_ t);
+      (* [Array1.init] requires a function *)
+      val_ "Bigarray.Array1.dim"           Array1.dim           (t @-> returning int);
+      (* [Array1.kind] returns an untestable value *)
+      (* [change_layout]: the layout is fixed in our sut, so we test a dummy version *)
+      val_ "Bigarray.Array1.change_layout" dummy_change_layout  (t @-> returning_ t);
+      val_ "Bigarray.Array1.size_in_bytes" Array1.size_in_bytes (t @-> returning int);
+      val_freq 4 "Bigarray.Array1.get"     Array1.get           (t @-> int @-> returning_or_exc int);
       val_ "Bigarray.Array1.set"           Array1.set           (t @-> int @-> int @-> returning_or_exc unit);
+      val_ "Bigarray.Array1.sub"           Array1.sub           (t @-> int @-> int @-> returning_or_exc_ t);
+      (* [Array1.slice]: cannot be tested since it produces a Bigarray.Array0.t *)
+      val_ "Bigarray.Array1.blit"          Array1.blit          (t @-> t @-> returning unit);
       val_ "Bigarray.Array1.fill"          Array1.fill          (t @-> int @-> returning unit);
+      val_ "Bigarray.Array1.of_array"      of_array             (bounded_array 100 int @-> returning_ t);
+      (* [Array1.unsafe_get] and [Array1.unsafe_set] cannot be tested:
+         they can segfault or produce any useless result *)
     ]
 end
 
diff --git a/src/bytes/lin_tests_dsl.ml b/src/bytes/lin_tests_dsl.ml
index 739974690..54c5c9dc8 100644
--- a/src/bytes/lin_tests_dsl.ml
+++ b/src/bytes/lin_tests_dsl.ml
@@ -3,17 +3,29 @@
 (* ********************************************************************** *)
 module BConf = struct
   type t = Bytes.t
-  let init () = Stdlib.Bytes.make 42 '0'
+  let init () = Bytes.make 42 '0'
   let cleanup _ = ()
 
   open Lin
+  let int = nat_small
+  let string = string_small
 
   let api = [
+    val_ "Bytes.length"      Bytes.length      (t @-> returning int);
     val_ "Bytes.get"         Bytes.get         (t @-> int @-> returning_or_exc char);
+    val_ "Bytes.set"         Bytes.set         (t @-> int @-> char @-> returning_or_exc unit);
+ (* val_ "Bytes.create"      Bytes.create      (int @-> returning_or_exc_ t); *) (* result contains arbitrary bytes, hence non-det. output! *)
+    val_ "Bytes.make"        Bytes.make        (int @-> char @-> returning_or_exc_ t);
+ (* val_ "Bytes.empty"       Bytes.empty       (returning_ t); *)
+    val_ "Bytes.copy"        Bytes.copy        (t @-> returning_ t);
+    val_ "Bytes.of_string"   Bytes.of_string   (string @-> returning_ t);
+    val_ "Bytes.to_string"   Bytes.to_string   (t @-> returning string);
     val_ "Bytes.sub_string"  Bytes.sub_string  (t @-> int @-> int @-> returning_or_exc string);
-    val_ "Bytes.length"      Bytes.length      (t @-> returning int);
-    val_ "Bytes.fill"        Bytes.fill        (t @-> int @-> int @-> char @-> returning_or_exc unit);
-    val_ "Bytes.blit_string" Bytes.blit_string (string @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
+    val_freq 2 "Bytes.fill"        Bytes.fill        (t @-> int @-> int @-> char @-> returning_or_exc unit);
+    val_freq 2 "Bytes.blit_string" Bytes.blit_string (string @-> int @-> t @-> int @-> int @-> returning_or_exc unit);
+    val_ "Bytes.trim"        Bytes.trim        (t @-> returning_ t);
+    val_ "Bytes.escaped"     Bytes.escaped     (t @-> returning_ t);
+    val_ "Bytes.index"       Bytes.index       (t @-> char @-> returning_or_exc int);
     val_ "Bytes.index_from"  Bytes.index_from  (t @-> int @-> char @-> returning_or_exc int)]
 end
 
@@ -21,6 +33,6 @@ module BT_domain = Lin_domain.Make(BConf)
 module BT_thread = Lin_thread.Make(BConf) [@alert "-experimental"]
 ;;
 QCheck_base_runner.run_tests_main [
-  BT_domain.lin_test ~count:1000 ~name:"Lin DSL Bytes test with Domain";
-  BT_thread.lin_test ~count:1000 ~name:"Lin DSL Bytes test with Thread";
+  BT_domain.neg_lin_test ~count:1000 ~name:"Lin DSL Bytes test with Domain";
+  BT_thread.lin_test     ~count:1000 ~name:"Lin DSL Bytes test with Thread";
 ]
diff --git a/src/hashtbl/dune b/src/hashtbl/dune
index b3373a377..367f64231 100644
--- a/src/hashtbl/dune
+++ b/src/hashtbl/dune
@@ -15,7 +15,7 @@
  (package multicoretests)
  (flags (:standard -w -27))
  (libraries qcheck-lin.domain)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq))
  ; (action (run %{test} --verbose))
  (action (echo "Skipping src/hashtbl/%{test} from the test suite\n\n"))
 )
diff --git a/src/hashtbl/lin_tests.ml b/src/hashtbl/lin_tests.ml
index f06e34c5d..663c22219 100644
--- a/src/hashtbl/lin_tests.ml
+++ b/src/hashtbl/lin_tests.ml
@@ -9,37 +9,65 @@ struct
   type t = (char, int) Hashtbl.t
 
   type cmd =
-    | Clear
-    | Add of char' * int'
-    | Remove of char'
-    | Find of char'
-    | Find_opt of char'
-    | Find_all of char'
-    | Replace of char' * int'
-    | Mem of char'
-    | Length [@@deriving qcheck, show { with_path = false }]
-  and int' = int [@gen Gen.nat]
-  and char' = char [@gen Gen.printable]
+    | Clear of Var.t
+    | Copy of Var.t
+    | Add of Var.t * char * int
+    | Remove of Var.t * char
+    | Find of Var.t * char
+    | Find_opt of Var.t * char
+    | Find_all of Var.t * char
+    | Replace of Var.t * char * int
+    | Mem of Var.t * char
+    | Length of Var.t [@@deriving show { with_path = false }]
+  let gen_int = Gen.nat
+  let gen_char = Gen.printable
 
-  let shrink_cmd c = match c with
-    | Clear -> Iter.empty
-    | Add (c,i) ->
-        Iter.((map (fun c -> Add (c,i)) (Shrink.char c))
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun v -> None,Clear v) gen_var;
+        map  (fun v -> Some (Var.next ()),Copy v) gen_var;
+        map3 (fun v c i -> None,Add (v,c,i)) gen_var gen_char gen_int;
+        map2 (fun v c -> None,Remove (v,c)) gen_var gen_char;
+        map2 (fun v c -> None,Find (v,c)) gen_var gen_char;
+        map2 (fun v c -> None,Find_opt (v,c)) gen_var gen_char;
+        map2 (fun v c -> None,Find_all (v,c)) gen_var gen_char;
+        map3 (fun v c i -> None,Replace (v,c,i)) gen_var gen_char gen_int;
+        map2 (fun v c -> None,Mem (v,c)) gen_var gen_char;
+        map  (fun v -> None,Length v) gen_var;
+      ])
+  let shrink_cmd _env c = match c with
+    | Clear _ -> Iter.empty
+    | Copy _ -> Iter.empty
+    | Add (v,c,i) ->
+        Iter.((map (fun c -> Add (v,c,i)) (Shrink.char c))
               <+>
-              (map (fun i -> Add (c,i)) (Shrink.int i)))
-    | Remove c -> Iter.map (fun c -> Remove c) (Shrink.char c)
-    | Find c -> Iter.map (fun c -> Find c) (Shrink.char c)
-    | Find_opt c -> Iter.map (fun c -> Find_opt c) (Shrink.char c)
-    | Find_all c -> Iter.map (fun c -> Find_all c) (Shrink.char c)
-    | Replace (c,i) ->
-        Iter.((map (fun c -> Replace (c,i)) (Shrink.char c))
+              (map (fun i -> Add (v,c,i)) (Shrink.int i)))
+    | Remove (v,c) -> Iter.map (fun c -> Remove (v,c)) (Shrink.char c)
+    | Find (v,c) -> Iter.map (fun c -> Find (v,c)) (Shrink.char c)
+    | Find_opt (v,c) -> Iter.map (fun c -> Find_opt (v,c)) (Shrink.char c)
+    | Find_all (v,c) -> Iter.map (fun c -> Find_all (v,c)) (Shrink.char c)
+    | Replace (v,c,i) ->
+        Iter.((map (fun c -> Replace (v,c,i)) (Shrink.char c))
               <+>
-              (map (fun i -> Replace (c,i)) (Shrink.int i)))
-    | Mem c -> Iter.map (fun c -> Mem c) (Shrink.char c)
-    | Length -> Iter.empty
+              (map (fun i -> Replace (v,c,i)) (Shrink.int i)))
+    | Mem (v,c) -> Iter.map (fun c -> Mem (v,c)) (Shrink.char c)
+    | Length _ -> Iter.empty
+
+  let cmd_uses_var v = function
+    | Clear i
+    | Copy i
+    | Add (i,_,_)
+    | Remove (i,_)
+    | Find (i,_)
+    | Find_opt (i,_)
+    | Find_all (i,_)
+    | Replace (i,_,_)
+    | Mem (i,_)
+    | Length i -> i=v
 
   type res =
     | RClear
+    | RCopy
     | RAdd
     | RRemove
     | RFind of ((int, exn) result [@equal (=)])
@@ -52,15 +80,17 @@ struct
   let init () = Hashtbl.create ~random:false 42
 
   let run c h = match c with
-    | Clear         -> Hashtbl.clear h; RClear
-    | Add (k,v)     -> Hashtbl.add h k v; RAdd
-    | Remove k      -> Hashtbl.remove h k; RRemove
-    | Find k        -> RFind (Util.protect (Hashtbl.find h) k)
-    | Find_opt k    -> RFind_opt (Hashtbl.find_opt h k)
-    | Find_all k    -> RFind_all (Hashtbl.find_all h k)
-    | Replace (k,v) -> Hashtbl.replace h k v; RReplace
-    | Mem k         -> RMem (Hashtbl.mem h k)
-    | Length        -> RLength (Hashtbl.length h)
+    | None, Clear w         -> Hashtbl.clear h.(w); RClear
+    | Some r, Copy w        -> let tmp = Hashtbl.copy h.(w) in h.(r) <- tmp; RCopy
+    | None, Add (w,k,v)     -> Hashtbl.add h.(w) k v; RAdd
+    | None, Remove (w,k)    -> Hashtbl.remove h.(w) k; RRemove
+    | None, Find (w,k)      -> RFind (Util.protect (fun () -> Hashtbl.find h.(w) k) ())
+    | None, Find_opt (w,k)  -> RFind_opt (Hashtbl.find_opt h.(w) k)
+    | None, Find_all (w,k)  -> RFind_all (Hashtbl.find_all h.(w) k)
+    | None, Replace (w,k,v) -> Hashtbl.replace h.(w) k v; RReplace
+    | None, Mem (w,k)       -> RMem (Hashtbl.mem h.(w) k)
+    | None, Length w        -> RLength (Hashtbl.length h.(w))
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end
diff --git a/src/hashtbl/lin_tests_dsl.ml b/src/hashtbl/lin_tests_dsl.ml
index 76b7b70a2..54f73f7bc 100644
--- a/src/hashtbl/lin_tests_dsl.ml
+++ b/src/hashtbl/lin_tests_dsl.ml
@@ -12,6 +12,7 @@ struct
   let int,char = nat_small,char_printable
   let api =
     [ val_ "Hashtbl.clear"    Hashtbl.clear    (t @-> returning unit);
+      val_ "Hashtbl.copy"     Hashtbl.copy     (t @-> returning_ t);
       val_ "Hashtbl.add"      Hashtbl.add      (t @-> char @-> int @-> returning unit);
       val_ "Hashtbl.remove"   Hashtbl.remove   (t @-> char @-> returning unit);
       val_ "Hashtbl.find"     Hashtbl.find     (t @-> char @-> returning_or_exc int);
diff --git a/src/io/dune b/src/io/dune
index 4985a5b0d..ffc745eb5 100644
--- a/src/io/dune
+++ b/src/io/dune
@@ -6,6 +6,7 @@
  (package multicoretests)
  ;(flags (:standard -w -27))
  (libraries qcheck-lin.domain)
+ (preprocess (pps ppx_deriving.show))
  ; (action (run %{test} --verbose))
  (action (echo "Skipping src/io/%{test} from the test suite\n\n"))
 )
diff --git a/src/io/lin_tests.ml b/src/io/lin_tests.ml
index de797dade..72b3b4632 100644
--- a/src/io/lin_tests.ml
+++ b/src/io/lin_tests.ml
@@ -12,26 +12,32 @@ let () =
   Out_channel.close out
 
 module In_channel_ops = struct
+  open Lin.Internal [@@alert "-internal"]
 
   type t = In_channel.t (* Filename and corresponding channel *)
 
-  type cmd = Close | Read of int | BlindRead of int
-
+  type cmd = Close of Var.t | Read of Var.t * int | BlindRead of Var.t * int [@@deriving show { with_path = false }]
+(*
   let show_cmd =
     let open Printf in function
     | Close -> "Close"
     | Read l -> sprintf "Read %d" l
     | BlindRead l -> sprintf "BlindRead %d" l
-
-  let gen_cmd =
+*)
+  let gen_cmd gen_var =
     let open QCheck.Gen in
     frequency
-      [1, return Close;
-       6, map (fun l -> Read l) small_nat;
-       6, map (fun l -> BlindRead l) small_nat;
+      [1, map  (fun v -> None, Close v) gen_var;
+       6, map2 (fun v l -> None, Read (v,l)) gen_var small_nat;
+       6, map2 (fun v l -> None, BlindRead (v,l)) gen_var small_nat;
       ]
 
-  let shrink_cmd _ = QCheck.Iter.empty
+  let shrink_cmd _env _ = QCheck.Iter.empty
+
+  let cmd_uses_var v = function
+    | Close i
+    | Read (i,_)
+    | BlindRead (i,_) -> i=v
 
   type res =
   | UnitRes of (unit, exn) result
@@ -55,41 +61,48 @@ module In_channel_ops = struct
 
   let run cmd chan =
     match cmd with
-    | Read l ->
-        begin try ReadRes (Ok (In_channel.really_input_string chan l))
+    | None, Read (i,l) ->
+        begin try ReadRes (Ok (In_channel.really_input_string chan.(i) l))
         with e -> ReadRes (Error e)
         end
-    | BlindRead l ->
-        begin try ignore (In_channel.really_input_string chan l); UnitRes (Ok ())
+    | None, BlindRead (i,l) ->
+        begin try ignore (In_channel.really_input_string chan.(i) l); UnitRes (Ok ())
         with e -> UnitRes (Error e)
         end
-    | Close ->
-        begin try In_channel.close chan; UnitRes (Ok ())
+    | None, Close i ->
+        begin try In_channel.close chan.(i); UnitRes (Ok ())
         with e -> UnitRes (Error e)
         end
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd cmd)))
 end
 
 module Out_channel_ops = struct
+  open Lin.Internal [@@alert "-internal"]
 
   type t = string * Out_channel.t (* Filename and corresponding channel *)
 
-  type cmd = Flush | Close | Write of string
-
+  type cmd = Flush of Var.t | Close of Var.t | Write of Var.t * string [@@deriving show { with_path = false }]
+(*
   let show_cmd =
     let open Printf in function
     | Flush -> "Flush"
     | Write s -> sprintf "Write %s" s
     | Close -> "Close"
-
-  let gen_cmd =
+*)
+  let gen_cmd gen_var =
     let open QCheck.Gen in
     frequency
-      [3, return Flush;
-       1, return Close;
-       6, map (fun s -> Write s) string;
+      [3, map  (fun i -> None,Flush i) gen_var;
+       1, map  (fun i -> None,Close i) gen_var;
+       6, map2 (fun i s -> None,Write (i,s)) gen_var string;
       ]
 
-  let shrink_cmd _ = QCheck.Iter.empty
+  let shrink_cmd _env _ = QCheck.Iter.empty
+
+  let cmd_uses_var v = function
+    | Flush i
+    | Close i
+    | Write (i,_) -> i=v
 
   type res = (unit, exn) result
 
@@ -108,20 +121,21 @@ module Out_channel_ops = struct
     Out_channel.close chan;
     try Sys.remove filename with Sys_error _ -> ()
 
-  let run cmd (_,chan) =
+  let run cmd chan =
     match cmd with
-    | Flush ->
-        begin try Out_channel.flush chan; Ok ()
+    | None, Flush i ->
+        begin try Out_channel.flush (snd chan.(i)); Ok ()
         with e -> Error e
         end
-    | Write s ->
-        begin try Out_channel.output_string chan s; Ok ()
+    | None, Write (i,s) ->
+        begin try Out_channel.output_string (snd chan.(i)) s; Ok ()
         with e -> Error e
         end
-    | Close ->
-        begin try Out_channel.close chan; Ok ()
+    | None, Close i ->
+        begin try Out_channel.close (snd chan.(i)); Ok ()
         with e -> Error e
         end
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd cmd)))
 end
 
 module Out_channel_lin = Lin_domain.Make_internal (Out_channel_ops) [@@alert "-internal"]
diff --git a/src/lazy/dune b/src/lazy/dune
index 937d13dd8..b76a97213 100644
--- a/src/lazy/dune
+++ b/src/lazy/dune
@@ -14,7 +14,7 @@
  (modules lin_tests)
  (package multicoretests)
  (libraries qcheck-lin.domain)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq))
  ; (action (run %{test} --verbose))
  (action (echo "Skipping src/lazy/%{test} from the test suite\n\n"))
 )
diff --git a/src/lazy/lin_tests.ml b/src/lazy/lin_tests.ml
index 1ae1b88f1..bf214f4f0 100644
--- a/src/lazy/lin_tests.ml
+++ b/src/lazy/lin_tests.ml
@@ -34,13 +34,23 @@ module LBase =
 struct
   open Lin.Internal [@@alert "-internal"]
   type cmd =
-    | Force
-    | Force_val
-    | Is_val
-    | Map of int_fun
-    | Map_val of int_fun [@@deriving qcheck, show { with_path = false }]
-  and int_fun = (int -> int) fun_ [@gen (fun1 Observable.int small_nat).gen][@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)]
+    | Force of Var.t
+    | Force_val of Var.t
+    | Is_val of Var.t
+    | Map of Var.t * int_fun
+    | Map_val of Var.t * int_fun [@@deriving show { with_path = false }]
+  and int_fun = (int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)]
 
+  let int_fun_gen = (fun1 Observable.int small_nat).gen
+
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun t -> None,Force t) gen_var;
+        map  (fun t -> None,Force_val t) gen_var;
+        map  (fun t -> None,Is_val t) gen_var;
+        map2 (fun t f -> None,Map (t,f)) gen_var int_fun_gen;
+        map2 (fun t f -> None,Map_val (t,f)) gen_var int_fun_gen;
+      ])
   (*
   let shrink_cmd c = match c with
     | Force
@@ -50,7 +60,14 @@ struct
     | Map_val f -> Iter.map (fun f -> Map_val f) (Fn.shrink f)
   *)
   (* the Lazy tests already take a while to run - so better avoid spending extra time shrinking *)
-  let shrink_cmd = Shrink.nil
+  let shrink_cmd _env = Shrink.nil
+
+  let cmd_uses_var v = function
+    | Force i
+    | Force_val i
+    | Is_val i
+    | Map (i,_)
+    | Map_val (i,_) -> i=v
 
   type t = int Lazy.t
 
@@ -65,13 +82,14 @@ struct
     | RMap_val of (int,exn) result [@@deriving show { with_path = false }, eq]
 
   let run c l = match c with
-    | Force               -> RForce (Util.protect Lazy.force l)
-    | Force_val           -> RForce_val (Util.protect Lazy.force_val l)
-    | Is_val              -> RIs_val (Lazy.is_val l)
-    | Map (Fun (_,f))     -> RMap (try Ok (Lazy.force (Lazy.map f l))
-                                   with exn -> Error exn) (*we force the "new lazy"*)
-    | Map_val (Fun (_,f)) -> RMap_val (try Ok (Lazy.force (Lazy.map_val f l))
-                                       with exn -> Error exn) (*we force the "new lazy"*)
+    | None,Force t               -> RForce (Util.protect Lazy.force l.(t))
+    | None,Force_val t           -> RForce_val (Util.protect Lazy.force_val l.(t))
+    | None,Is_val t              -> RIs_val (Lazy.is_val l.(t))
+    | None,Map (t,Fun (_,f))     -> RMap (try Ok (Lazy.force (Lazy.map f l.(t)))
+                                          with exn -> Error exn) (*we force the "new lazy"*)
+    | None,Map_val (t,Fun (_,f)) -> RMap_val (try Ok (Lazy.force (Lazy.map_val f l.(t)))
+                                              with exn -> Error exn) (*we force the "new lazy"*)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 
 
diff --git a/src/neg_tests/dune b/src/neg_tests/dune
index 7c36a7454..6cec8b606 100644
--- a/src/neg_tests/dune
+++ b/src/neg_tests/dune
@@ -61,7 +61,7 @@
  (modules lin_tests_common)
  (package multicoretests)
  (libraries CList qcheck-lin.domain)
- (preprocess (pps ppx_deriving_qcheck ppx_deriving.show ppx_deriving.eq))
+ (preprocess (pps ppx_deriving.show ppx_deriving.eq))
 )
 
 (test
diff --git a/src/neg_tests/lin_tests_common.ml b/src/neg_tests/lin_tests_common.ml
index d0ea882e5..bc2a7cc04 100644
--- a/src/neg_tests/lin_tests_common.ml
+++ b/src/neg_tests/lin_tests_common.ml
@@ -24,66 +24,106 @@ module Sut_int64 =
 end
 
 module RConf_int = struct
+  open Lin
+  open Internal [@@alert "-internal"]
+
   type t = int ref
 
   type cmd =
-    | Get
-    | Set of int'
-    | Add of int'
-    | Incr
-    | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = int [@gen Gen.nat]
-
-  let shrink_cmd c = match c with
-    | Get
-    | Incr
-    | Decr -> Iter.empty
-    | Set i -> Iter.map (fun i -> Set i) (Shrink.int i)
-    | Add i -> Iter.map (fun i -> Add i) (Shrink.int i)
+    | Get of Var.t
+    | Set of Var.t * int
+    | Add of Var.t * int
+    | Incr of Var.t
+    | Decr of Var.t [@@deriving show { with_path = false }]
+
+  let gen_int = Gen.nat
+  let gen_cmd gen_var =
+    Gen.(oneof[
+        map  (fun t -> None,Get t) gen_var;
+        map2 (fun t i -> None,Set (t,i)) gen_var gen_int;
+        map2 (fun t i -> None,Add (t,i)) gen_var gen_int;
+        map  (fun t -> None,Incr t) gen_var;
+        map  (fun t -> None,Decr t) gen_var;
+      ])
+
+  let shrink_cmd _env c = match c with
+    | Get _
+    | Incr _
+    | Decr _ -> Iter.empty
+    | Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int i)
+    | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int i)
+
+  let cmd_uses_var v = function
+    | Get i
+    | Set (i,_)
+    | Add (i,_)
+    | Incr i
+    | Decr i -> i=v
 
   type res = RGet of int | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
   let init () = Sut_int.init ()
 
   let run c r = match c with
-    | Get   -> RGet (Sut_int.get r)
-    | Set i -> (Sut_int.set r i; RSet)
-    | Add i -> (Sut_int.add r i; RAdd)
-    | Incr  -> (Sut_int.incr r; RIncr)
-    | Decr  -> (Sut_int.decr r; RDecr)
+    | None,Get t     -> RGet (Sut_int.get r.(t))
+    | None,Set (t,i) -> (Sut_int.set r.(t) i; RSet)
+    | None,Add (t,i) -> (Sut_int.add r.(t) i; RAdd)
+    | None,Incr t    -> (Sut_int.incr r.(t); RIncr)
+    | None,Decr t    -> (Sut_int.decr r.(t); RDecr)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end
 
 
 module RConf_int64 = struct
+  open Lin
+  open Internal [@@alert "-internal"]
+
   type t = int64 ref
 
   type cmd =
-    | Get
-    | Set of int'
-    | Add of int'
-    | Incr
-    | Decr [@@deriving qcheck, show { with_path = false }]
-  and int' = int64 [@gen Gen.(map Int64.of_int nat)]
-
-  let shrink_cmd c = match c with
-    | Get
-    | Incr
-    | Decr -> Iter.empty
-    | Set i -> Iter.map (fun i -> Set i) (Shrink.int64 i)
-    | Add i -> Iter.map (fun i -> Add i) (Shrink.int64 i)
+    | Get of Var.t
+    | Set of Var.t * int64
+    | Add of Var.t * int64
+    | Incr of Var.t
+    | Decr of Var.t [@@deriving show { with_path = false }]
+
+  let gen_int64 = Gen.(map Int64.of_int nat)
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map  (fun t -> None,Get t) gen_var;
+        map2 (fun t i -> None,Set (t,i)) gen_var gen_int64;
+        map2 (fun t i -> None,Add (t,i)) gen_var gen_int64;
+        map  (fun t -> None,Incr t) gen_var;
+        map  (fun t -> None,Decr t) gen_var;
+      ])
+
+  let shrink_cmd _env c = match c with
+    | Get _
+    | Incr _
+    | Decr _ -> Iter.empty
+    | Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int64 i)
+    | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int64 i)
+
+  let cmd_uses_var v = function
+    | Get i
+    | Set (i,_)
+    | Add (i,_)
+    | Incr i
+    | Decr i -> i=v
 
   type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
   let init () = Sut_int64.init ()
 
   let run c r = match c with
-    | Get   -> RGet (Sut_int64.get r)
-    | Set i -> (Sut_int64.set r i; RSet)
-    | Add i -> (Sut_int64.add r i; RAdd)
-    | Incr  -> (Sut_int64.incr r; RIncr)
-    | Decr  -> (Sut_int64.decr r; RDecr)
+    | None,Get t     -> RGet (Sut_int64.get r.(t))
+    | None,Set (t,i) -> (Sut_int64.set r.(t) i; RSet)
+    | None,Add (t,i) -> (Sut_int64.add r.(t) i; RAdd)
+    | None,Incr t    -> (Sut_int64.incr r.(t); RIncr)
+    | None,Decr t    -> (Sut_int64.decr r.(t); RDecr)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end
@@ -111,20 +151,31 @@ struct
   let pp_int' fmt t = Format.fprintf fmt "%s" (T.to_string t)
 
   type cmd =
-    | Add_node of int'
-    | Member of int' [@@deriving qcheck, show { with_path = false }]
+    | Add_node of Lin.Var.t * int'
+    | Member of Lin.Var.t * int' [@@deriving show { with_path = false }]
+
+  let gen_cmd gen_var =
+    Gen.(oneof [
+        map2 (fun t i -> None,Add_node (t,i)) gen_var gen_int';
+        map2 (fun t i -> None,Member (t,i)) gen_var gen_int';
+      ])
+
+  let shrink_cmd _env c = match c with
+    | Add_node (t,i) -> Iter.map (fun i -> Add_node (t,i)) (T.shrink i)
+    | Member (t,i) -> Iter.map (fun i -> Member (t,i)) (T.shrink i)
 
-  let shrink_cmd c = match c with
-    | Add_node i -> Iter.map (fun i -> Add_node i) (T.shrink i)
-    | Member i -> Iter.map (fun i -> Member i) (T.shrink i)
+  let cmd_uses_var v = function
+    | Add_node (i,_)
+    | Member (i,_) -> v=i
 
   type res = RAdd_node of bool | RMember of bool [@@deriving show { with_path = false }, eq]
 
   let init () = CList.list_init T.zero
 
   let run c r = match c with
-    | Add_node i -> RAdd_node (CList.add_node r i)
-    | Member i   -> RMember (CList.member r i)
+    | None,Add_node (t,i) -> RAdd_node (CList.add_node r.(t) i)
+    | None,Member (t,i)   -> RMember (CList.member r.(t) i)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 
   let cleanup _ = ()
 end
diff --git a/src/neg_tests/lin_tests_effect.ml b/src/neg_tests/lin_tests_effect.ml
index cc1ba48d6..0458db8ef 100644
--- a/src/neg_tests/lin_tests_effect.ml
+++ b/src/neg_tests/lin_tests_effect.ml
@@ -14,11 +14,12 @@ struct
   type res = RGet of int | RSet | RAdd of (unit,exn) result | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
   let run c r = match c with
-    | Get   -> RGet (Sut_int.get r)
-    | Set i -> (Sut_int.set r i; RSet)
-    | Add i -> (try let tmp = Sut_int.get r in Lin_effect.yield (); Sut_int.set r (tmp+i); RAdd (Ok ()) with exn -> RAdd (Error exn))
-    | Incr  -> (Sut_int.incr r; RIncr)
-    | Decr  -> (Sut_int.decr r; RDecr)
+    | None,Get t     -> RGet (Sut_int.get r.(t))
+    | None,Set (t,i) -> (Sut_int.set r.(t) i; RSet)
+    | None,Add (t,i) -> (try let tmp = Sut_int.get r.(t) in Lin_effect.yield (); Sut_int.set r.(t) (tmp+i); RAdd (Ok ()) with exn -> RAdd (Error exn))
+    | None,Incr t    -> (Sut_int.incr r.(t); RIncr)
+    | None,Decr t    -> (Sut_int.decr r.(t); RDecr)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 
 module RT_int_effect = Lin_effect.Make_internal(RConf_int) [@alert "-internal"]
@@ -30,11 +31,12 @@ struct
   type res = RGet of int64 | RSet | RAdd of (unit,exn) result | RIncr | RDecr [@@deriving show { with_path = false }, eq]
 
   let run c r = match c with
-    | Get   -> RGet (Sut_int64.get r)
-    | Set i -> (Sut_int64.set r i; RSet)
-    | Add i -> (try let tmp = Sut_int.get r in Lin_effect.yield (); Sut_int.set r (Int64.add tmp i); RAdd (Ok ()) with exn -> RAdd (Error exn))
-    | Incr  -> (Sut_int64.incr r; RIncr)
-    | Decr  -> (Sut_int64.decr r; RDecr)
+    | None,Get t     -> RGet (Sut_int64.get r.(t))
+    | None,Set (t,i) -> (Sut_int64.set r.(t) i; RSet)
+    | None,Add (t,i) -> (try let tmp = Sut_int.get r.(t) in Lin_effect.yield (); Sut_int.set r.(t) (Int64.add tmp i); RAdd (Ok ()) with exn -> RAdd (Error exn))
+    | None,Incr t    -> (Sut_int64.incr r.(t); RIncr)
+    | None,Decr t    -> (Sut_int64.decr r.(t); RDecr)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 module RT_int64_effect = Lin_effect.Make_internal(RConf_int64) [@alert "-internal"]
 module RT_int64'_effect = Lin_effect.Make_internal(RConf_int64') [@alert "-internal"]
@@ -44,8 +46,9 @@ struct
   include CLConf(Int)
   type res = RAdd_node of (bool,exn) result | RMember of bool [@@deriving show { with_path = false }, eq]
   let run c r = match c with
-    | Add_node i -> RAdd_node (try Lin_effect.yield (); Ok (CList.add_node r i) with exn -> Error exn)
-    | Member i   -> RMember (CList.member r i)
+    | None,Add_node (t,i) -> RAdd_node (try Lin_effect.yield (); Ok (CList.add_node r.(t) i) with exn -> Error exn)
+    | None,Member (t,i)   -> RMember (CList.member r.(t) i)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 module CLT_int_effect = Lin_effect.Make_internal(CLConf (Int)) [@alert "-internal"]
 module CLT_int'_effect = Lin_effect.Make_internal(CLConf_int') [@alert "-internal"]
@@ -55,8 +58,9 @@ struct
   include CLConf(Int64)
   type res = RAdd_node of (bool,exn) result | RMember of bool [@@deriving show { with_path = false }, eq]
   let run c r = match c with
-    | Add_node i -> RAdd_node (try Lin_effect.yield (); Ok (CList.add_node r i) with exn -> Error exn)
-    | Member i   -> RMember (CList.member r i)
+    | None,Add_node (t,i) -> RAdd_node (try Lin_effect.yield (); Ok (CList.add_node r.(t) i) with exn -> Error exn)
+    | None,Member (t,i)   -> RMember (CList.member r.(t) i)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 module CLT_int64_effect = Lin_effect.Make_internal(CLConf(Int64)) [@alert "-internal"]
 module CLT_int64'_effect = Lin_effect.Make_internal(CLConf_int64') [@alert "-internal"]
diff --git a/src/queue/lin_tests.ml b/src/queue/lin_tests.ml
index 489b5e4b7..3a5743283 100644
--- a/src/queue/lin_tests.ml
+++ b/src/queue/lin_tests.ml
@@ -4,35 +4,59 @@ open Lin.Internal [@@alert "-internal"]
 module Spec =
   struct
     type t = int Queue.t
-    let m = Mutex.create ()
 
     type cmd =
-      | Add of int'
-      | Take
-      | Take_opt
-      | Peek
-      | Peek_opt
-      | Clear
-      | Is_empty
-      | Fold of fct * int'
-      | Length [@@deriving qcheck, show { with_path = false }]
-    and int' = int [@gen Gen.nat]
-    and fct = (int -> int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)] [@gen (fun2 Observable.int Observable.int small_int).gen]
+      | Add of Var.t * int
+      | Take of Var.t
+      | Take_opt of Var.t
+      | Peek of Var.t
+      | Peek_opt of Var.t
+      | Clear of Var.t
+      | Is_empty of Var.t
+      | Fold of Var.t * fct * int
+      | Length of Var.t [@@deriving show { with_path = false }]
+    and fct = (int -> int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)]
+
+    let gen_int = Gen.nat
+    let gen_fct = (fun2 Observable.int Observable.int small_int).gen
+    let gen_cmd gen_var =
+      Gen.(oneof [
+          map2 (fun t i -> None,Add (t,i)) gen_var gen_int;
+          map  (fun t -> None, Take t) gen_var;
+          map  (fun t -> None, Take_opt t) gen_var;
+          map  (fun t -> None, Peek t) gen_var;
+          map  (fun t -> None, Peek_opt t) gen_var;
+          map  (fun t -> None, Clear t) gen_var;
+          map  (fun t -> None, Is_empty t) gen_var;
+          map3 (fun t f i -> None,Fold (t,f,i)) gen_var gen_fct gen_int;
+          map  (fun t -> None, Length t) gen_var;
+        ])
 
-    let shrink_cmd c = match c with
-      | Take
-      | Take_opt
-      | Peek
-      | Peek_opt
-      | Clear
-      | Is_empty
-      | Length -> Iter.empty
-      | Add i -> Iter.map (fun i -> Add i) (Shrink.int i)
-      | Fold (f,i) ->
+    let shrink_cmd _env c = match c with
+      | Take _
+      | Take_opt _
+      | Peek _
+      | Peek_opt _
+      | Clear _
+      | Is_empty _
+      | Length _ -> Iter.empty
+      | Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int i)
+      | Fold (t,f,i) ->
           Iter.(
-            (map (fun f -> Fold (f,i)) (Fn.shrink f))
+            (map (fun f -> Fold (t,f,i)) (Fn.shrink f))
             <+>
-            (map (fun i -> Fold (f,i)) (Shrink.int i)))
+            (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
+
+    let cmd_uses_var v = function
+      | Add (i,_)
+      | Take i
+      | Take_opt i
+      | Peek i
+      | Peek_opt i
+      | Clear i
+      | Is_empty i
+      | Fold (i,_,_)
+      | Length i -> i=v
 
     type res =
       | RAdd
@@ -53,56 +77,59 @@ module QConf =
   struct
     include Spec
     let run c q = match c with
-      | Add i       -> Queue.add i q; RAdd
-      | Take        -> RTake (Util.protect Queue.take q)
-      | Take_opt    -> RTake_opt (Queue.take_opt q)
-      | Peek        -> RPeek (Util.protect Queue.peek q)
-      | Peek_opt    -> RPeek_opt (Queue.peek_opt q)
-      | Length      -> RLength (Queue.length q)
-      | Is_empty    -> RIs_empty (Queue.is_empty q)
-      | Fold (f, a) -> RFold (Queue.fold (Fn.apply f) a q)
-      | Clear       -> Queue.clear q; RClear
+      | None,Add (t,i)    -> Queue.add i q.(t); RAdd
+      | None,Take t       -> RTake (Util.protect Queue.take q.(t))
+      | None,Take_opt t   -> RTake_opt (Queue.take_opt q.(t))
+      | None,Peek t       -> RPeek (Util.protect Queue.peek q.(t))
+      | None,Peek_opt t   -> RPeek_opt (Queue.peek_opt q.(t))
+      | None,Length t     -> RLength (Queue.length q.(t))
+      | None,Is_empty t   -> RIs_empty (Queue.is_empty q.(t))
+      | None,Fold (t,f,a) -> RFold (Queue.fold (Fn.apply f) a q.(t))
+      | None,Clear t      -> Queue.clear q.(t); RClear
+      | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
    end
 
 module QMutexConf =
   struct
     include Spec
+    let m = Mutex.create ()
     let run c q = match c with
-      | Add i       -> Mutex.lock m;
-                       Queue.add i q;
-                       Mutex.unlock m; RAdd
-      | Take        -> Mutex.lock m;
-                       let r = Util.protect Queue.take q in
-                       Mutex.unlock m;
-                       RTake r
-      | Take_opt    -> Mutex.lock m;
-                       let r = Queue.take_opt q in
-                       Mutex.unlock m;
-                       RTake_opt r
-      | Peek        -> Mutex.lock m;
-                       let r = Util.protect Queue.peek q in
-                       Mutex.unlock m;
-                       RPeek r
-      | Peek_opt    -> Mutex.lock m;
-                       let r = Queue.peek_opt q in
-                       Mutex.unlock m;
-                       RPeek_opt r
-      | Length      -> Mutex.lock m;
-                       let l = Queue.length q in
-                       Mutex.unlock m;
-                       RLength l
-      | Is_empty    -> Mutex.lock m;
-                       let b = Queue.is_empty q in
-                       Mutex.unlock m;
-                       RIs_empty b
-      | Fold (f, a) -> Mutex.lock m;
-                       let r = (Queue.fold (Fn.apply f) a q)  in
-                       Mutex.unlock m;
-                       RFold r
-      | Clear       -> Mutex.lock m;
-                       Queue.clear q;
-                       Mutex.unlock m;
-                       RClear
+      | None,Add (t,i)    -> Mutex.lock m;
+                             Queue.add i q.(t);
+                             Mutex.unlock m; RAdd
+      | None,Take t       -> Mutex.lock m;
+                             let r = Util.protect Queue.take q.(t) in
+                             Mutex.unlock m;
+                             RTake r
+      | None,Take_opt t   -> Mutex.lock m;
+                             let r = Queue.take_opt q.(t) in
+                             Mutex.unlock m;
+                             RTake_opt r
+      | None,Peek t       -> Mutex.lock m;
+                             let r = Util.protect Queue.peek q.(t) in
+                             Mutex.unlock m;
+                             RPeek r
+      | None,Peek_opt t   -> Mutex.lock m;
+                             let r = Queue.peek_opt q.(t) in
+                             Mutex.unlock m;
+                             RPeek_opt r
+      | None,Length t     -> Mutex.lock m;
+                             let l = Queue.length q.(t) in
+                             Mutex.unlock m;
+                             RLength l
+      | None,Is_empty t   -> Mutex.lock m;
+                             let b = Queue.is_empty q.(t) in
+                             Mutex.unlock m;
+                             RIs_empty b
+      | None,Fold (t,f,a) -> Mutex.lock m;
+                             let r = (Queue.fold (Fn.apply f) a q.(t))  in
+                             Mutex.unlock m;
+                             RFold r
+      | None,Clear t      -> Mutex.lock m;
+                             Queue.clear q.(t);
+                             Mutex.unlock m;
+                             RClear
+      | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 
 module QMT_domain = Lin_domain.Make_internal(QMutexConf) [@alert "-internal"]
diff --git a/src/stack/dune b/src/stack/dune
index ac02856a6..2fa43c929 100644
--- a/src/stack/dune
+++ b/src/stack/dune
@@ -19,4 +19,3 @@
   ; (action (run %{test} --verbose))
  (action (echo "Skipping src/stack/%{test} from the test suite\n\n"))
 )
-
diff --git a/src/stack/lin_tests.ml b/src/stack/lin_tests.ml
index afda8e1dc..8098abe44 100644
--- a/src/stack/lin_tests.ml
+++ b/src/stack/lin_tests.ml
@@ -4,35 +4,60 @@ open Lin.Internal [@@alert "-internal"]
 module Spec =
   struct
     type t = int Stack.t
-    let m = Mutex.create ()
 
     type cmd =
-      | Push of int'
-      | Pop
-      | Pop_opt
-      | Top
-      | Top_opt
-      | Clear
-      | Is_empty
-      | Fold of fct * int'
-      | Length [@@deriving qcheck, show { with_path = false }]
-    and int' = int [@gen Gen.nat]
-    and fct = (int -> int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)] [@gen (fun2 Observable.int Observable.int small_int).gen]
+      | Push of Var.t * int
+      | Pop of Var.t
+      | Pop_opt of Var.t
+      | Top of Var.t
+      | Top_opt of Var.t
+      | Clear of Var.t
+      | Is_empty of Var.t
+      | Fold of Var.t * fct * int
+      | Length of Var.t [@@deriving show { with_path = false }]
+    and fct = (int -> int -> int) fun_ [@printer fun fmt f -> fprintf fmt "%s" (Fn.print f)]
+
+    let gen_int = Gen.nat
+    let gen_fct = (fun2 Observable.int Observable.int small_int).gen
+
+    let gen_cmd gen_var =
+      Gen.(oneof [
+          map2 (fun t i -> None,Push (t,i)) gen_var gen_int;
+          map  (fun t -> None, Pop t) gen_var;
+          map  (fun t -> None, Pop_opt t) gen_var;
+          map  (fun t -> None, Top t) gen_var;
+          map  (fun t -> None, Top_opt t) gen_var;
+          map  (fun t -> None, Clear t) gen_var;
+          map  (fun t -> None, Is_empty t) gen_var;
+          map3 (fun t f i -> None,Fold (t,f,i)) gen_var gen_fct gen_int;
+          map  (fun t -> None, Length t) gen_var;
+        ])
 
-    let shrink_cmd c = match c with
-      | Pop
-      | Pop_opt
-      | Top
-      | Top_opt
-      | Clear
-      | Is_empty
-      | Length -> Iter.empty
-      | Push i -> Iter.map (fun i -> Push i) (Shrink.int i)
-      | Fold (f,i) ->
+    let shrink_cmd _env c = match c with
+      | Pop _
+      | Pop_opt _
+      | Top _
+      | Top_opt _
+      | Clear _
+      | Is_empty _
+      | Length _ -> Iter.empty
+      | Push (t,i) -> Iter.map (fun i -> Push (t,i)) (Shrink.int i)
+      | Fold (t,f,i) ->
           Iter.(
-            (map (fun f -> Fold (f,i)) (Fn.shrink f))
+            (map (fun f -> Fold (t,f,i)) (Fn.shrink f))
             <+>
-            (map (fun i -> Fold (f,i)) (Shrink.int i)))
+            (map (fun i -> Fold (t,f,i)) (Shrink.int i)))
+
+    let cmd_uses_var v c = match c with
+      | Push (i,_)
+      | Pop i
+      | Pop_opt i
+      | Top i
+      | Top_opt i
+      | Clear i
+      | Is_empty i
+      | Fold (i,_,_)
+      | Length i -> i=v
 
     type res =
       | RPush
@@ -53,56 +78,59 @@ module SConf =
   struct
     include Spec
     let run c s = match c with
-      | Push i      -> Stack.push i s; RPush
-      | Pop         -> RPop (Util.protect Stack.pop s)
-      | Pop_opt     -> RPop_opt (Stack.pop_opt s)
-      | Top         -> RTop (Util.protect Stack.top s)
-      | Top_opt     -> RTop_opt (Stack.top_opt s)
-      | Clear       -> Stack.clear s; RClear
-      | Is_empty    -> RIs_empty (Stack.is_empty s)
-      | Fold (f, a) -> RFold (Stack.fold (Fn.apply f) a s)
-      | Length      -> RLength (Stack.length s)
+      | None,Push (t,i)   -> Stack.push i s.(t); RPush
+      | None,Pop t        -> RPop (Util.protect Stack.pop s.(t))
+      | None,Pop_opt t    -> RPop_opt (Stack.pop_opt s.(t))
+      | None,Top t        -> RTop (Util.protect Stack.top s.(t))
+      | None,Top_opt t    -> RTop_opt (Stack.top_opt s.(t))
+      | None,Clear t      -> Stack.clear s.(t); RClear
+      | None,Is_empty t   -> RIs_empty (Stack.is_empty s.(t))
+      | None,Fold (t,f,a) -> RFold (Stack.fold (Fn.apply f) a s.(t))
+      | None,Length t     -> RLength (Stack.length s.(t))
+      | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
   end
 
 module SMutexConf =
   struct
     include Spec
+    let m = Mutex.create ()
     let run c s = match c with
-      | Push i      -> Mutex.lock m;
-                       Stack.push i s;
-                       Mutex.unlock m; RPush
-      | Pop         -> Mutex.lock m;
-                       let r = Util.protect Stack.pop s in
-                       Mutex.unlock m;
-                       RPop r
-      | Pop_opt     -> Mutex.lock m;
-                       let r = Stack.pop_opt s in
-                       Mutex.unlock m;
-                       RPop_opt r
-      | Top         -> Mutex.lock m;
-                       let r = Util.protect Stack.top s in
-                       Mutex.unlock m;
-                       RTop r
-      | Top_opt     -> Mutex.lock m;
-                       let r = Stack.top_opt s in
-                       Mutex.unlock m;
-                       RTop_opt r
-      | Clear       -> Mutex.lock m;
-                       Stack.clear s;
-                       Mutex.unlock m;
-                       RClear
-      | Is_empty    -> Mutex.lock m;
-                       let b = Stack.is_empty s in
-                       Mutex.unlock m;
-                       RIs_empty b
-      | Fold (f, a) -> Mutex.lock m;
-                       let r  = Stack.fold (Fn.apply f) a s in
-                       Mutex.unlock m;
-                       RFold r
-      | Length      -> Mutex.lock m;
-                       let l = Stack.length s in
-                       Mutex.unlock m;
-                       RLength l
+      | None,Push (t,i)   -> Mutex.lock m;
+                             Stack.push i s.(t);
+                             Mutex.unlock m; RPush
+      | None,Pop t        -> Mutex.lock m;
+                             let r = Util.protect Stack.pop s.(t) in
+                             Mutex.unlock m;
+                             RPop r
+      | None,Pop_opt t    -> Mutex.lock m;
+                             let r = Stack.pop_opt s.(t) in
+                             Mutex.unlock m;
+                             RPop_opt r
+      | None,Top t        -> Mutex.lock m;
+                             let r = Util.protect Stack.top s.(t) in
+                             Mutex.unlock m;
+                             RTop r
+      | None,Top_opt t    -> Mutex.lock m;
+                             let r = Stack.top_opt s.(t) in
+                             Mutex.unlock m;
+                             RTop_opt r
+      | None,Clear t      -> Mutex.lock m;
+                             Stack.clear s.(t);
+                             Mutex.unlock m;
+                             RClear
+      | None,Is_empty t   -> Mutex.lock m;
+                             let b = Stack.is_empty s.(t) in
+                             Mutex.unlock m;
+                             RIs_empty b
+      | None,Fold (t,f,a) -> Mutex.lock m;
+                             let r  = Stack.fold (Fn.apply f) a s.(t) in
+                             Mutex.unlock m;
+                             RFold r
+      | None,Length t     -> Mutex.lock m;
+                             let l = Stack.length s.(t) in
+                             Mutex.unlock m;
+                             RLength l
+      | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
   end
 
 module ST_domain = Lin_domain.Make_internal(SConf) [@alert "-internal"]
diff --git a/test/cleanup_lin.ml b/test/cleanup_lin.ml
index 23e25728c..a64e4a667 100644
--- a/test/cleanup_lin.ml
+++ b/test/cleanup_lin.ml
@@ -7,25 +7,32 @@ let cleanup_counter = Atomic.make 0
 
 module RConf =
 struct
+  open Lin.Internal [@@alert "-internal"]
+
   exception Already_cleaned
   type status = Inited | Cleaned
 
   type cmd =
-    | Get
-    | Set of int
-    | Add of int [@@deriving show { with_path = false }]
+    | Get of Var.t
+    | Set of Var.t * int
+    | Add of Var.t * int [@@deriving show { with_path = false }]
 
   type t = (status ref) * (int ref)
 
-  let gen_cmd =
+  let gen_cmd gen_var =
     let int_gen = Gen.nat in
       (Gen.oneof
-         [Gen.return Get;
-	  Gen.map (fun i -> Set i) int_gen;
-	  Gen.map (fun i -> Add i) int_gen;
+         [Gen.map  (fun t ->   None, Get t) gen_var;
+	  Gen.map2 (fun t i -> None, Set (t,i)) gen_var int_gen;
+	  Gen.map2 (fun t i -> None, Add (t,i)) gen_var int_gen;
          ])
 
-  let shrink_cmd = Shrink.nil
+  let shrink_cmd _env = Shrink.nil
+
+  let cmd_uses_var v = function
+    | Get i
+    | Set (i,_)
+    | Add (i,_) -> i=v
 
   let init () =
     Atomic.incr cleanup_counter ;
@@ -39,10 +46,11 @@ struct
 
   type res = RGet of int | RSet | RAdd [@@deriving show { with_path = false }, eq]
 
-  let run c (_,r) = match c with
-    | Get   -> RGet (!r)
-    | Set i -> (r:=i; RSet)
-    | Add i -> (let old = !r in r := i + old; RAdd) (* buggy: not atomic *)
+  let run c s = match c with
+    | None, Get t     -> RGet (!(snd s.(t)))
+    | None, Set (t,i) -> ((snd s.(t)):=i; RSet)
+    | None, Add (t,i) -> (let old = !(snd (s.(t))) in snd (s.(t)) := i + old; RAdd) (* buggy: not atomic *)
+    | _, _ -> failwith (Printf.sprintf "unexpected command: %s" (show_cmd (snd c)))
 end
 
 module RT = Lin_domain.Make_internal(RConf) [@alert "-internal"]