diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index 5272d97dfde85f7bccbd98fa0757734441d61b3b..eb593e762bfc2efa349c5f801f96e5f2b7214962 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -40,13 +40,7 @@ struct
   let ty_fst_arg = function
     | Some l :: _ -> l
     | _ -> raise Not_found
-    (*
-  let l_havoc = Qed.Engine.F_call "havoc"
-  let f_havoc =
-    Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
-  let havoc fresh current loc n =
-    Lang.F.e_fun f_havoc [fresh;current;loc;n]
-  *)
+
   let l_memcpy = Qed.Engine.F_call "memcpy"
   let f_memcpy =
     Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_memcpy "memcpy"
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 438544bbf54dc63807d5373e7c97de7b7f42af72..d1bd6baa7932cc751c7a8275c0d3611b1999cb9c 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -636,7 +636,13 @@ struct
     | C_comp _ | C_array _ ->
       Set(load_init seq.post obj loc, value) :: memcpy_init seq obj loc
 
-  let copied s obj p q = stored s obj p (load_value s.pre obj q)
+  let copied s obj p q = match obj with
+    | C_int _ | C_float _ | C_pointer _ ->
+      stored s obj p (load_value s.pre obj q)
+    | C_comp _ | C_array _ ->
+      Set(load_value s.post obj p, load_value s.pre obj q)
+      :: memcpy s obj ~lsrc:q p
+
 
   let copied_init s obj p q = stored_init s obj p (load_init s.pre obj q)
 
@@ -652,11 +658,12 @@ struct
       [ updated_init_atom seq obj loc (e_var init) ;
         updated_atom seq obj loc (e_var value) ]
     | C_comp _ | C_array _ ->
-      memcpy seq obj loc @ memcpy_init seq obj loc
+      memcpy seq obj ~lsrc:loc loc @ memcpy_init seq obj loc
 
   let assigned_range s obj l a b =
-    memcpy_length s obj (M.shift l obj a) (e_range a b) @
-    memcpy_init_length s obj (M.shift l obj a) (e_range a b)
+    let loc = M.shift l obj a in
+    memcpy_length s obj loc (e_range a b) @
+    memcpy_init_length s obj loc (e_range a b)
 
   let assigned seq obj sloc =
     (* Assert (M.monotonic_init seq.pre seq.post) :: *)
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 93e0f2287f014d9a9af7fcb35ec99c1b5c8b42d4..78a20c8d1fcfca9e9f3d401373c1a597b9249bc7 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -35,12 +35,11 @@ let ty_fst_arg = function
   | Some l :: _ -> l
   | _ -> raise Not_found
 
-(* let l_havoc = Qed.Engine.F_call "havoc"*)
+
 let l_memcpy = Qed.Engine.F_call "memcpy"
 let l_set_init = Qed.Engine.F_call "set_init"
 
 let p_eqmem = Lang.extern_fp ~library "eqmem"
-(* let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc" *)
 let f_memcpy = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_memcpy "memcpy"
 let p_framed = Lang.extern_fp ~coloring:true ~library "framed" (* m-pointer -> prop *)
 let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst" (* int-memory -> prop *)
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 609645de518dbb5875238884204c76013add7b22..da6c1eb517d8301ac608d05618628a2f5121e394 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -195,7 +195,7 @@ sig
 
       Memory chunk variables are assigned lazily. Hence, the vector is
       empty unless a chunk is accessed. Pay attention to this
-      when you merge or havoc chunks.
+      when you merge or havoc chunks (using memcpy).
 
       New chunks are generated from the context pool of {!Lang.freshvar}.
   *)