diff --git a/regression/cbmc-library/tolower-01/main.c b/regression/cbmc-library/tolower-01/main.c
index cf7c6f12611..8e528b4a9e1 100644
--- a/regression/cbmc-library/tolower-01/main.c
+++ b/regression/cbmc-library/tolower-01/main.c
@@ -3,7 +3,8 @@
 
 int main()
 {
-  tolower();
-  assert(0);
+  int x;
+  int r = tolower(x);
+  assert(r >= x);
   return 0;
 }
diff --git a/regression/cbmc-library/tolower-01/test.desc b/regression/cbmc-library/tolower-01/test.desc
index 9542d988e8d..96c9b4bcd7b 100644
--- a/regression/cbmc-library/tolower-01/test.desc
+++ b/regression/cbmc-library/tolower-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/toupper-01/main.c b/regression/cbmc-library/toupper-01/main.c
index 4891a936b74..3b98daecf37 100644
--- a/regression/cbmc-library/toupper-01/main.c
+++ b/regression/cbmc-library/toupper-01/main.c
@@ -3,7 +3,8 @@
 
 int main()
 {
-  toupper();
-  assert(0);
+  int x;
+  int r = toupper(x);
+  assert(r <= x);
   return 0;
 }
diff --git a/regression/cbmc-library/toupper-01/test.desc b/regression/cbmc-library/toupper-01/test.desc
index 9542d988e8d..96c9b4bcd7b 100644
--- a/regression/cbmc-library/toupper-01/test.desc
+++ b/regression/cbmc-library/toupper-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/src/ansi-c/library/ctype.c b/src/ansi-c/library/ctype.c
index e7bfb4461ad..294c54e1e44 100644
--- a/src/ansi-c/library/ctype.c
+++ b/src/ansi-c/library/ctype.c
@@ -95,12 +95,52 @@ int isupper(int c)
 int isxdigit(int c)
 { return (c>='A' && c<='F') || (c>='a' && c<='f') || (c>='0' && c<='9'); }
 
+/* FUNCTION: __CPROVER_tolower */
+
+int __CPROVER_tolower(int c)
+{
+  return (c >= 'A' && c <= 'Z') ? c + ('a' - 'A') : c;
+}
+
 /* FUNCTION: tolower */
 
+int __CPROVER_tolower(int c);
+
 int tolower(int c)
-{ return (c>='A' && c<='Z')?c+('a'-'A'):c; }
+{
+  return __CPROVER_tolower(c);
+}
+
+/* FUNCTION: __tolower */
+
+int __CPROVER_tolower(int c);
+
+int __tolower(int c)
+{
+  return __CPROVER_tolower(c);
+}
+
+/* FUNCTION: __CPROVER_toupper */
+
+int __CPROVER_toupper(int c)
+{
+  return (c >= 'a' && c <= 'z') ? c - ('a' - 'A') : c;
+}
 
 /* FUNCTION: toupper */
 
+int __CPROVER_toupper(int c);
+
 int toupper(int c)
-{ return (c>='a' && c<='z')?c-('a'-'A'):c; }
+{
+  return __CPROVER_toupper(c);
+}
+
+/* FUNCTION: __toupper */
+
+int __CPROVER_toupper(int c);
+
+int __toupper(int c)
+{
+  return __CPROVER_toupper(c);
+}
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index b6ee26d03f7..7e2fd2fe11f 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -54,9 +54,12 @@ perl -p -i -e 's/^__stdio_common_vsprintf\n//' __functions # snprintf, Windows
 perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
 perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
 perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD
+perl -p -i -e 's/^__tolower\n//' __functions # tolower, macOS
+perl -p -i -e 's/^__toupper\n//' __functions # toupper, macOS
 
 # Some functions are covered by existing tests:
 perl -p -i -e 's/^__CPROVER_(creat|fcntl|open|openat)\n//' __functions # creat, fcntl, open, openat
+perl -p -i -e 's/^__CPROVER_(tolower|toupper)\n//' __functions # tolower, toupper
 perl -p -i -e 's/^(creat|fcntl|open|openat)64\n//' __functions # same as creat, fcntl, open, openat
 perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
 perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01