diff --git a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.c b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.c
new file mode 100644
index 00000000000..4b080a1c267
--- /dev/null
+++ b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.c
@@ -0,0 +1,17 @@
+#include <stdlib.h>
+
+int main(void)
+{
+  void *ptr = malloc(sizeof(char));
+  if(ptr == NULL)
+    return 0;
+
+  void *ptr1 = realloc(ptr, 2 * sizeof(char));
+  if(ptr1 == NULL)
+  {
+    free(ptr);
+    return 0;
+  }
+
+  free(ptr1);
+}
diff --git a/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc
new file mode 100644
index 00000000000..a5bf8ec70eb
--- /dev/null
+++ b/regression/cbmc/realloc-should-not-free-on-failure-to-allocate/test.desc
@@ -0,0 +1,11 @@
+CORE
+test.c
+--malloc-may-fail --malloc-fail-null
+^\[main.precondition_instance.\d+] line \d+ double free: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This is a test checking for a regression where the --malloc-may-fail flag
+introduced a double-free bug in the stdlib models with realloc.
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 2bf24fdc654..aa0d1a49991 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -477,8 +477,10 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
   void *res;
   res=malloc(malloc_size);
   if(res != (void *)0)
+  {
     __CPROVER_array_copy(res, ptr);
-  free(ptr);
+    free(ptr);
+  }
 
   return res;
 }