diff --git a/regression/cbmc/posix_memalign/main.c b/regression/cbmc/posix_memalign/main.c
new file mode 100644
index 00000000000..1d0a76e901c
--- /dev/null
+++ b/regression/cbmc/posix_memalign/main.c
@@ -0,0 +1,16 @@
+#include <stdlib.h>
+#include <string.h>
+
+int main()
+{
+  size_t size = 4;
+  size_t page_size = 4096;
+  void *src = "testing";
+  void *dest;
+  if(posix_memalign(&dest, page_size, size))
+  {
+    return -1;
+  }
+  memcpy(dest, src, size);
+  return 0;
+}
diff --git a/regression/cbmc/posix_memalign/test.desc b/regression/cbmc/posix_memalign/test.desc
new file mode 100644
index 00000000000..3e2ef98ab4b
--- /dev/null
+++ b/regression/cbmc/posix_memalign/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^\*\*\*\* WARNING: no body for function posix_memalign