diff --git a/regression/goto-instrument/slice22/main.c b/regression/goto-instrument/slice22/main.c
new file mode 100644
index 00000000000..bac167b63d3
--- /dev/null
+++ b/regression/goto-instrument/slice22/main.c
@@ -0,0 +1,19 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int *ptr=malloc(sizeof(int));
+  *ptr=42;
+  ptr=realloc(ptr, 20);
+  assert(*ptr==42);
+
+  int *ptr2=malloc(2*sizeof(int));
+  *ptr2=42;
+  *(ptr2+1)=42;
+  ptr2=realloc(ptr2, 20);
+  assert(*ptr2==42);
+  assert(*(ptr2+1)==42);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice22/test.desc b/regression/goto-instrument/slice22/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice22/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-instrument/slice23/main.c b/regression/goto-instrument/slice23/main.c
new file mode 100644
index 00000000000..d165e2c38b8
--- /dev/null
+++ b/regression/goto-instrument/slice23/main.c
@@ -0,0 +1,25 @@
+#include <stdlib.h>
+#include <assert.h>
+
+void foo(int argc)
+{
+  void* x=0;
+
+  if(argc>3)
+    x=malloc(4*sizeof(int));
+  else
+    x=malloc(3*sizeof(int));
+  *(int*)x=42;
+
+  x=realloc(x, sizeof(int));
+
+  assert(*(int*)x==42);
+}
+
+int main(int argc, char* argv[])
+{
+//__CPROVER_ASYNC_1:
+  foo(argc);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice23/test.desc b/regression/goto-instrument/slice23/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice23/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 59bda7f0af0..f7b42a0af3c 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -337,6 +337,10 @@ static bool implicit(goto_programt::const_targett target)
 {
   // some variables are used during symbolic execution only
 
+  const irep_idt &statement=target->code.get_statement();
+  if(statement==ID_array_copy)
+    return true;
+
   if(!target->is_assign())
     return false;
 
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 125a2cae58a..55542296c48 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1729,6 +1729,9 @@ void value_set_fit::apply_code(
   else if(statement==ID_fence)
   {
   }
+  else if(statement==ID_array_copy)
+  {
+  }
   else if(statement==ID_input || statement==ID_output)
   {
     // doesn't do anything