diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 26913e6..7a8e5a6 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -323,11 +323,12 @@ struct
   let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
     match state with (mem, types, vals) ->
     let x = pathvar p in
-    let id = vals_assoc x vals in
-    let b = pathval mem vals p in
-    let t' = pathtype types p in
-    let (mem', b') = valspoil mem b t t' m Rf in
-    let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in
+    let id = vals_assoc x vals in (* base var address *)
+    let b = pathval mem vals p in (* subvalue in var *)
+    let t' = pathtype types p in (* type of subvalue *)
+    let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
+    (* TODO: FIXME: why copy (Cp)? *)
+    let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in (* set subvalue into var *)
     mem_set mem'' id v''
 
   let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
@@ -394,8 +395,10 @@ struct
                             let (mem', v') = valupd mem (mem_get mem id) p ZeroV in
                             (mem_set mem' id v', types, vals)
                      | _ -> raise @@ Eval_error "write: type")
-    | ReadS p -> if pathval mem vals p != ZeroV
-                 then raise @@ Eval_error "read"
+    | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV 
+                 then raise @@ Eval_error "read: spoiled value"
+                 else if pathval mem vals p != ZeroV 
+                 then raise @@ Eval_error "read: nontrivial value"
                  else state
     | SeqS (sl, sr) -> let statel = stmt_eval state sl in
                        stmt_eval statel sr
@@ -429,12 +432,18 @@ struct
   let v3 = VarP 3
   let v4 = VarP 4
   let v5 = VarP 5
-  let vg0 = VarP (globals_min_id)
+  let v6 = VarP 6
+  let v7 = VarP 7
+  let v8 = VarP 8
+  let vg0 = VarP globals_min_id
   let vg1 = VarP (globals_min_id + 1)
   let vg2 = VarP (globals_min_id + 2)
   let vg3 = VarP (globals_min_id + 3)
   let vg4 = VarP (globals_min_id + 4)
   let vg5 = VarP (globals_min_id + 5)
+  let vg6 = VarP (globals_min_id + 6)
+  let vg7 = VarP (globals_min_id + 7)
+  let vg8 = VarP (globals_min_id + 8)
 
   let rf0E = RefE 0
   let rf1E = RefE 1
@@ -442,12 +451,19 @@ struct
   let rf3E = RefE 3
   let rf4E = RefE 4
   let rf5E = RefE 5
+  let rf3E = RefE 3
+  let rf4E = RefE 4
+  let rf5E = RefE 5
   let rfg0E = RefE globals_min_id
   let rfg1E = RefE (globals_min_id + 1)
   let rfg2E = RefE (globals_min_id + 2)
   let rfg3E = RefE (globals_min_id + 3)
   let rfg4E = RefE (globals_min_id + 4)
   let rfg5E = RefE (globals_min_id + 5)
+  let rfg6E = RefE (globals_min_id + 6)
+  let rfg7E = RefE (globals_min_id + 7)
+  let rfg8E = RefE (globals_min_id + 8)
+
   let pE p = PathE p
 
   let drf p = DerefP p
@@ -511,7 +527,7 @@ struct
     try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id));
          [%expect.unreachable]);
     with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| read |}]
+    [%expect {| read: spoiled value |}]
 
   let%expect_test "simple vars, no read & read" =
     prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
@@ -649,7 +665,7 @@ struct
     );
     [%expect.unreachable]);
     with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| read |}]
+    [%expect {| read: spoiled value |}]
 
   let%expect_test "call inside call, dsl" =
     prog_eval_noret (
@@ -695,7 +711,7 @@ struct
         defgu uT_r_aw;
         defg (rfT uT_r_aw) rfg0E;
         defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r_aw) rfg2E;
         FunD (
           [
             moded @@ rfT @@ uT_r;
@@ -710,6 +726,76 @@ struct
     Printf.printf "done!";
     [%expect {| done! |}]
 
+  let%expect_test "simple call with different arguments modifiers, copy, dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg0E;
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg2E;
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg4E;
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg6E;
+        FunD (
+          [
+            ((NIn, NOut), cpT @@ uT_aw);
+            ((In, NOut), cpT @@ uT_r_aw);
+            ((NIn, Out), cpT @@ uT_aw);
+            ((In, Out), cpT @@ uT_r_aw);
+          ],
+          (rdS @@ drf @@ v1) #.
+          (rdS @@ drf @@ v3) #.
+          (wrS @@ drf @@ v1) #.
+          (wrS @@ drf @@ v2) #.
+          (wrS @@ drf @@ v3)
+        )
+      ],
+      (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
+      (rdS @@ drf @@ vg1) #.
+      (rdS @@ drf @@ vg3) #.
+      (rdS @@ drf @@ vg5) #.
+      (rdS @@ drf @@ vg7)
+    );
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple call with different arguments modifiers, ref, dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg0E;
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg2E;
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg4E;
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg6E;
+        FunD (
+          [
+            ((NIn, NOut), rfT @@ uT);
+            ((In, NOut), rfT @@ uT_r);
+            ((NIn, Out), rfT @@ uT_aw);
+            ((In, Out), rfT @@ uT_r_aw);
+          ],
+          (rdS @@ drf @@ v1) #.
+          (rdS @@ drf @@ v3) #.
+          (wrS @@ drf @@ v2) #.
+          (wrS @@ drf @@ v3)
+        )
+      ],
+      (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
+      (rdS @@ drf @@ vg1) #.
+      (rdS @@ drf @@ vg3) #.
+      (rdS @@ drf @@ vg5) #.
+      (rdS @@ drf @@ vg7)
+    );
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* TODO: call after call test (fix test) *)
+  (* TODO: recursive call test (for the future when memoization will be implemented) *)
+
   (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
 
   (* --- tests --- *)
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 7d3c8b4..edfcf3d 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -906,9 +906,10 @@ $s in stmt, f in X, x in X, a in X$
     $l = vals[x]$,
     $vals, mu texpre p eqmu b$,
     $types ttype p : t'$,
-    // TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs
+    // TODO: FIXME: Ref or Copy ?? in root <- Copy ??,
+    // <- otherwise all subsequent copy capabilities will be ref (in current impl)
     // FIXME depends on parent ??
-    $cl b, mu cr xarrowSquiggly(t \, t' \, m \, Ref)_spoil cl b', mu' cr$,
+    $cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$,
     $cl mu'[l], mu' cr xarrowSquiggly(cl p \, b' cr)_modify cl v'', mu'' cr$,
 
     $mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
@@ -920,7 +921,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ full spoil for tuple expr],
+    name: [ full spoil for ref expr],
 
     // NOTE: x as path
     $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
@@ -941,7 +942,7 @@ $s in stmt, f in X, x in X, a in X$
     $...$,
     $mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,
 
-    $mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n]_(cl vals, types cr) mu_n$,
+    $mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n])_(cl vals, types cr) mu_n$,
   )
 ))
 
diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 1ce75a1..31a1e70 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -717,7 +717,7 @@ struct
       vals_assoco x vals id &
       pathvalo mem vals p b &
       pathtypeo types p tp' &
-      valspoilo mem b tp tp' m Rf(Std.pair mem_sp b_sp) &
+      valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) &
       mem_geto mem_sp id v_sp &
       valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) &
       mem_seto mem_upd id v_upd mem'