diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index c9ca9fc31..0012963c4 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -36,7 +36,16 @@ bool assertions_enabled() {
     return g_enable_assertions;
 }
 
+static atomic<bool> g_enable_notify_assertion_violation(true);
+
+void disable_notify_assertion_violation() {
+    g_enable_notify_assertion_violation = false;
+}
+
+
 void notify_assertion_violation(const char * fileName, int line, const char * condition) {
+    if (!g_enable_notify_assertion_violation)
+        return;
     std::cerr << "ASSERTION VIOLATION\n"
                  "File: " << fileName << "\n"
                  "Line: " << line << '\n'
diff --git a/src/util/debug.h b/src/util/debug.h
index 5f092b181..6ee0d6c8d 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -67,6 +67,7 @@ void invoke_gdb();
 #endif
 
 void notify_assertion_violation(const char * file_name, int line, const char * condition);
+void disable_notify_assertion_violation();
 void enable_debug(const char * tag);
 void disable_debug(const char * tag);
 bool is_debug_enabled(const char * tag);
diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp
index c030c2ec6..8045022e8 100644
--- a/src/util/timeout.cpp
+++ b/src/util/timeout.cpp
@@ -25,6 +25,7 @@ Revision History:
 
 #include "util/event_handler.h"
 #include "util/scoped_timer.h"
+#include "util/debug.h"
 
 static scoped_timer * g_timeout = nullptr;
 static void (* g_on_timeout)() = nullptr;
@@ -36,6 +37,7 @@ public:
         m_caller_id = caller_id;
         std::cout << "timeout\n";
         std::cout.flush();
+        disable_notify_assertion_violation();
         if (g_on_timeout)
             g_on_timeout();
         throw z3_error(ERR_TIMEOUT);