diff --git a/COMPILING.md b/COMPILING.md
index d83e6f3818e..e4e5dece720 100644
--- a/COMPILING.md
+++ b/COMPILING.md
@@ -255,6 +255,14 @@ require manual modification of build files.
    to generate IDE projects by supplying the `-G` flag.  Run `cmake -G` for a
    comprehensive list of supported back-ends.
 
+   On macOS >10.14, the build will fail unless you explicitly specify
+   the full path to the compiler. This issue is being tracked
+   [here](https://github.com/diffblue/cbmc/issues/4956). The invocation thus
+   looks like this:
+   ```
+   cmake -S. -Bbuild -DCMAKE_C_COMPILER=/usr/bin/clang
+   ```
+
    Generally it is not necessary to manually specify individual compiler or
    linker flags, as CMake defines a number of "build modes" including Debug and
    Release modes. To build in a particular mode, add the flag