diff --git a/src/ansi-c/library/mman.c b/src/ansi-c/library/mman.c
index d751454d802..4c96a423f89 100644
--- a/src/ansi-c/library/mman.c
+++ b/src/ansi-c/library/mman.c
@@ -20,6 +20,7 @@
 #  endif
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+void *mmap64(void *, __CPROVER_size_t, int, int, int, off_t);
 
 void *mmap(
   void *addr,
@@ -29,24 +30,7 @@ void *mmap(
   int fd,
   off_t offset)
 {
-  (void)prot;
-  (void)fd;
-  (void)offset;
-
-  if(
-    addr == 0 ||
-    (__VERIFIER_nondet___CPROVER_bool() && (flags & MAP_FIXED) == 0))
-  {
-    if(flags & MAP_ANONYMOUS && (flags & MAP_UNINITIALIZED) == 0)
-      return __CPROVER_allocate(length, 1);
-    else
-      return __CPROVER_allocate(length, 0);
-  }
-  else
-  {
-    __CPROVER_allocated_memory((__CPROVER_size_t)addr, length);
-    return addr;
-  }
+  return mmap64(addr, length, prot, flags, fd, offset);
 }
 
 #endif
@@ -73,6 +57,7 @@ void *mmap(
 #  endif
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+void *mmap64(void *, __CPROVER_size_t, int, int, int, off_t);
 
 void *_mmap(
   void *addr,
@@ -81,6 +66,42 @@ void *_mmap(
   int flags,
   int fd,
   off_t offset)
+{
+  return mmap64(addr, length, prot, flags, fd, offset);
+}
+
+#endif
+
+/* FUNCTION: mmap64 */
+
+#ifndef _WIN32
+
+#  ifndef __CPROVER_SYS_MMAN_H_INCLUDED
+#    include <sys/mman.h>
+#    define __CPROVER_SYS_MMAN_H_INCLUDED
+#  endif
+
+#  ifndef MAP_FIXED
+#    define MAP_FIXED 0
+#  endif
+
+#  ifndef MAP_ANONYMOUS
+#    define MAP_ANONYMOUS 0
+#  endif
+
+#  ifndef MAP_UNINITIALIZED
+#    define MAP_UNINITIALIZED 0
+#  endif
+
+__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
+
+void *mmap64(
+  void *addr,
+  __CPROVER_size_t length,
+  int prot,
+  int flags,
+  int fd,
+  off_t offset)
 {
   (void)prot;
   (void)fd;
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index ecea459eb89..7390554a256 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -57,6 +57,7 @@ perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01
 perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen
 perl -p -i -e 's/^fopen64\n//' __functions # fopen
 perl -p -i -e 's/^freopen64\n//' __functions # freopen
+perl -p -i -e 's/^mmap64\n//' __functions # mmap
 perl -p -i -e 's/^munmap\n//' __functions # mmap-01
 perl -p -i -e 's/^__fgets_chk\n//' __functions # fgets-01/__fgets_chk.desc
 perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf-01/__fprintf_chk.desc