diff --git a/src/math/polysat/log.cpp b/src/math/polysat/log.cpp
index b61171c1c..143272300 100644
--- a/src/math/polysat/log.cpp
+++ b/src/math/polysat/log.cpp
@@ -5,6 +5,7 @@
 #include <io.h>
 #undef min
 #endif
+#include <atomic>
 #include <utility>
 
 #include "util/util.h"
@@ -25,6 +26,12 @@ Other:
 
 #if POLYSAT_LOGGING_ENABLED
 
+std::atomic<bool> g_log_enabled(true);
+
+void set_log_enabled(bool log_enabled) {
+  g_log_enabled = log_enabled;
+}
+
 static LogLevel get_max_log_level(std::string const& fn, std::string const& pretty_fn) {
   (void)fn;
   (void)pretty_fn;
@@ -45,20 +52,23 @@ static LogLevel get_max_log_level(std::string const& fn, std::string const& pret
 
 /// Filter log messages
 bool polysat_should_log(LogLevel msg_level, std::string fn, std::string pretty_fn) {
+  if (!g_log_enabled)
+    return false;
   LogLevel max_log_level = get_max_log_level(fn, pretty_fn);
   return msg_level <= max_log_level;
 }
 
+char const* color_red()    { return "\x1B[31m"; }
+char const* color_yellow() { return "\x1B[33m"; }
+char const* color_blue()   { return "\x1B[34m"; }
+char const* color_reset()  { return "\x1B[0m"; }
+
 static char const* level_color(LogLevel msg_level) {
   switch (msg_level) {
-    case LogLevel::Heading1:
-      return ""; // red
-    case LogLevel::Heading2:
-      return ""; // yellow
-    case LogLevel::Heading3:
-      return ""; // blue
-    default:
-      return nullptr;
+    case LogLevel::Heading1: return color_red();
+    case LogLevel::Heading2: return color_yellow();
+    case LogLevel::Heading3: return color_blue();
+    default: return nullptr;
   }
 }
 
diff --git a/src/math/polysat/log.h b/src/math/polysat/log.h
index dbd734b33..b44fc226c 100644
--- a/src/math/polysat/log.h
+++ b/src/math/polysat/log.h
@@ -18,8 +18,15 @@
 #endif
 
 
+char const* color_blue();
+char const* color_yellow();
+char const* color_red();
+char const* color_reset();
+
+
 #if POLYSAT_LOGGING_ENABLED
 
+void set_log_enabled(bool log_enabled);
 
 class polysat_log_indent
 {
@@ -57,9 +64,8 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
       std::ostream& os = pair.first;                               \
       bool should_reset = pair.second;                             \
       os << x;                                                     \
-      if (should_reset) {                                          \
-        os << "\x1B[0m"; /* reset color */                         \
-      }                                                            \
+      if (should_reset)                                            \
+        os << color_reset();                                       \
       os << std::endl;                                             \
     }                                                              \
   } while (false)
@@ -87,6 +93,7 @@ polysat_log(LogLevel msg_level, std::string fn, std::string pretty_fn);
 
 #else  // POLYSAT_LOGGING_ENABLED
 
+void set_log_enabled(bool) {}
 
 #define LOG_(lvl, x)  \
   do {               \