diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 781eae51c..4544fec27 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -130,6 +130,7 @@ Version 4.17.0
   https://github.com/Z3Prover/z3/pull/9303
 - Add fold-unfold tactic as an alternative to solve-eqs for variable elimination using
   fold-unfold transformations. Also exposed as a simplifier.
+- Handle SIGXCPU (OS timeout) like a regular `-T` timeout.  Users should make sure to set the soft limit below the hard one, as in `ulimit -S -t 30 -H -t 31` for a 30s soft limit, so SIGXCPU is delivered before SIGKILL.
 
 Version 4.16.0
 ==============
diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp
index c030c2ec6..f640db1a5 100644
--- a/src/util/timeout.cpp
+++ b/src/util/timeout.cpp
@@ -19,6 +19,7 @@ Revision History:
 
 --*/
 #include<iostream>
+#include<signal.h>
 #include "util/util.h"
 #include "util/timeout.h"
 #include "util/error_codes.h"
@@ -29,15 +30,28 @@ Revision History:
 static scoped_timer * g_timeout = nullptr;
 static void (* g_on_timeout)() = nullptr;
 
+static void do_timeout() {
+    std::cout << "timeout\n";
+    std::cout.flush();
+    if (g_on_timeout)
+        g_on_timeout();
+}
+
+#ifdef SIGXCPU
+// React to SIGXCPU (an external CPU limit, e.g. ulimit -t) like a -T timeout.
+static void STD_CALL on_sigxcpu(int) {
+    signal(SIGXCPU, SIG_DFL);
+    do_timeout();
+    raise(SIGXCPU);
+}
+#endif
+
 namespace {
 class g_timeout_eh : public event_handler {
 public:
     void operator()(event_handler_caller_t caller_id) override {
         m_caller_id = caller_id;
-        std::cout << "timeout\n";
-        std::cout.flush();
-        if (g_on_timeout)
-            g_on_timeout();
+        do_timeout();
         throw z3_error(ERR_TIMEOUT);
     }
 };
@@ -56,4 +70,8 @@ void disable_timeout() {
 
 void register_on_timeout_proc(void (*proc)()) {
     g_on_timeout = proc;
+#ifdef SIGXCPU
+    // Handle external CPU limits (SIGXCPU) like our own timeouts.
+    signal(SIGXCPU, on_sigxcpu);
+#endif
 }