diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 83c0e2772..1ba82408b 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include<sstream>
+#include<format>
 #include "ast/bv_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "util/warning.h"
@@ -672,9 +673,11 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         }
         for (unsigned i = 0; i < num_args; ++i) {
             if (args[i]->get_sort() != r->get_domain(i)) {
-                std::ostringstream buffer;
-                buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " has sort " << mk_pp(args[i]->get_sort(), m) << " it does not match declaration " << mk_pp(r, m);
-                m.raise_exception(buffer.str());
+                m.raise_exception(std::format("Argument {} at position {} has sort {} it does not match declaration {}",
+                                               to_string(mk_pp(args[i], m)),
+                                               i,
+                                               to_string(mk_pp(args[i]->get_sort(), m)),
+                                               to_string(mk_pp(r, m))));
                 return nullptr;
             }
         }
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index fc3ddfcab..4b4a4568b 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -17,6 +17,8 @@ Revision History:
 
 --*/
 
+#include<sstream>
+#include<format>
 #include "util/warning.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
@@ -377,10 +379,9 @@ namespace datatype {
                 return nullptr;
             }
             if (rng != domain[1]) {
-                std::ostringstream buffer;
-                buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) 
-                       << " instead of " << mk_ismt2_pp(domain[1], m);
-                m.raise_exception(buffer.str());
+                m.raise_exception(std::format("second argument to field update should be {} instead of {}",
+                                               to_string(mk_ismt2_pp(rng, m)),
+                                               to_string(mk_ismt2_pp(domain[1], m))));
                 return nullptr;
             }
             range = domain[0];
diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
index a63d13f59..19ae67fd5 100644
--- a/src/ast/dl_decl_plugin.cpp
+++ b/src/ast/dl_decl_plugin.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include<sstream>
+#include<format>
 
 #include "ast/ast_pp.h"
 #include "ast/array_decl_plugin.h"
@@ -52,9 +53,7 @@ namespace datalog {
         if (low <= val && val <= up) {
             return true;
         }
-        std::ostringstream buffer;
-        buffer << msg << ", value is not within bound " << low << " <= " << val << " <= " << up;
-        m_manager->raise_exception(buffer.str());
+        m_manager->raise_exception(std::format("{}, value is not within bound {} <= {} <= {}", msg, low, val, up));
         return false;
     }
 
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 16c7e3492..aa8683f83 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include <sstream>
+#include <format>
 
 
 seq_decl_plugin::seq_decl_plugin(): m_init(false),
@@ -82,10 +83,8 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor
     ptr_vector<sort> binding;
     ast_manager& m = *m_manager;
     if (dsz == 0) {
-        std::ostringstream strm;
-        strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
-        strm << "at least one argument expected " << dsz << " given";
-        m.raise_exception(strm.str());
+        m.raise_exception(std::format("Unexpected number of arguments to '{}' at least one argument expected {} given",
+                                       sig.m_name.str(), dsz));
     }
     bool is_match = true;
     for (unsigned i = 0; is_match && i < dsz; ++i) {
@@ -96,16 +95,16 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor
         is_match = match(binding, range, sig.m_range);
     }
     if (!is_match) {
-        std::ostringstream strm;
-        strm << "Sort of function '" << sig.m_name << "' ";
-        strm << "does not match the declared type. Given domain: ";
+        std::string domain_str;
         for (unsigned i = 0; i < dsz; ++i) {
-            strm << mk_pp(dom[i], m) << " ";
+            domain_str += to_string(mk_pp(dom[i], m)) + " ";
         }
+        std::string range_str;
         if (range) {
-            strm << " and range: " << mk_pp(range, m);
+            range_str = std::format(" and range: {}", to_string(mk_pp(range, m)));
         }
-        m.raise_exception(strm.str());
+        m.raise_exception(std::format("Sort of function '{}' does not match the declared type. Given domain: {}{}",
+                                       sig.m_name.str(), domain_str, range_str));
     }
     range_out = apply_binding(binding, sig.m_range);
     SASSERT(range_out);
@@ -115,10 +114,8 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
     m_binding.reset();
     ast_manager& m = *m_manager;
     if (sig.m_dom.size() != dsz) {
-        std::ostringstream strm;
-        strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
-        strm << sig.m_dom.size() << " arguments expected " << dsz << " given";
-        m.raise_exception(strm.str());
+        m.raise_exception(std::format("Unexpected number of arguments to '{}' {} arguments expected {} given",
+                                       sig.m_name.str(), sig.m_dom.size(), dsz));
     }
     bool is_match = true;
     for (unsigned i = 0; is_match && i < dsz; ++i) {
@@ -128,28 +125,25 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
         is_match = match(m_binding, range, sig.m_range);
     }
     if (!is_match) {
-        std::ostringstream strm;
-        strm << "Sort of polymorphic function '" << sig.m_name << "' ";
-        strm << "does not match the declared type. ";
-        strm << "\nGiven domain: ";
+        std::string given_domain;
         for (unsigned i = 0; i < dsz; ++i) {
-            strm << mk_pp(dom[i], m) << " ";
+            given_domain += to_string(mk_pp(dom[i], m)) + " ";
         }
+        std::string range_str;
         if (range) {
-            strm << " and range: " << mk_pp(range, m);
+            range_str = std::format(" and range: {}", to_string(mk_pp(range, m)));
         }
-        strm << "\nExpected domain: ";
+        std::string expected_domain;
         for (unsigned i = 0; i < dsz; ++i) {
-            strm << mk_pp(sig.m_dom[i].get(), m) << " ";
+            expected_domain += to_string(mk_pp(sig.m_dom[i].get(), m)) + " ";
         }
 
-        m.raise_exception(strm.str());
+        m.raise_exception(std::format("Sort of polymorphic function '{}' does not match the declared type. \nGiven domain: {}{}\nExpected domain: {}",
+                                       sig.m_name.str(), given_domain, range_str, expected_domain));
     }
     if (!range && dsz == 0) {
-        std::ostringstream strm;
-        strm << "Sort of polymorphic function '" << sig.m_name << "' ";
-        strm << "is ambiguous. Function takes no arguments and sort of range has not been constrained";
-        m.raise_exception(strm.str());
+        m.raise_exception(std::format("Sort of polymorphic function '{}' is ambiguous. Function takes no arguments and sort of range has not been constrained",
+                                       sig.m_name.str()));
     }
     range_out = apply_binding(m_binding, sig.m_range);
     SASSERT(range_out);