diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp
index f1b56a0d54..08ebf4261e 100644
--- a/src/library/io_state.cpp
+++ b/src/library/io_state.cpp
@@ -81,15 +81,14 @@ scope_global_ios::~scope_global_ios() {
     g_ios = m_old_ios;
 }
 
-MK_THREAD_LOCAL_GET_DEF(std::string, get_what_str);
-
 char const * formatted_exception::what() const noexcept {
-    options const & opts = get_global_ios().get_options();
-    std::ostringstream out;
-    out << mk_pair(m_fmt, opts);
-    std::string & r = get_what_str();
-    r = out.str();
-    return r.c_str();
+    if (!m_what_buffer) {
+        options const & opts = get_global_ios().get_options();
+        std::ostringstream out;
+        out << mk_pair(m_fmt, opts);
+        const_cast<formatted_exception*>(this)->m_what_buffer = out.str();
+    }
+    return m_what_buffer->c_str();
 }
 
 options const & get_options_from_ios(io_state const & ios) {
diff --git a/src/library/io_state.h b/src/library/io_state.h
index 3eb7df2d26..211cb13215 100644
--- a/src/library/io_state.h
+++ b/src/library/io_state.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-
+#include <string>
 #include "util/output_channel.h"
 #include "util/sexpr/options.h"
 #include "util/exception_with_pos.h"
@@ -61,8 +61,9 @@ io_state const & get_global_ios();
     This is slightly different from ext_exception where the format object is built on demand. */
 class formatted_exception : public exception_with_pos {
 protected:
-    optional<pos_info> m_pos;
-    format             m_fmt;
+    optional<pos_info>    m_pos;
+    format                m_fmt;
+    optional<std::string> m_what_buffer;
 public:
     explicit formatted_exception(format const & fmt):m_fmt(fmt) {}
     formatted_exception(optional<pos_info> const & p, format const & fmt):m_pos(p), m_fmt(fmt) {}