From 241d77185ad9e2d2c42be19cf4cb75e1056f9b0d Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 10 Jul 2026 22:10:41 +0000 Subject: [PATCH] Fix Mac Build x64 CI failure: replace std::format with string concatenation std::format requires MACOSX_DEPLOYMENT_TARGET >= 13.3 because libc++'s header includes floating-point formatters that use std::to_chars, which was only introduced in macOS 13.3. The Mac Build x64 CI job targets macOS 13.0, causing compilation errors. Fix: Replace all std::format() calls in the affected files with equivalent string concatenation using std::to_string() for integers and the + operator for strings. Also remove the now-unnecessary #include from each file. --- src/ast/array_decl_plugin.cpp | 30 +++++++++++------------------- src/ast/ast.cpp | 32 +++++++------------------------- src/ast/bv_decl_plugin.cpp | 7 +------ src/ast/datatype_decl_plugin.cpp | 5 +---- src/ast/dl_decl_plugin.cpp | 3 +-- src/ast/seq_decl_plugin.cpp | 21 ++++++++------------- 6 files changed, 29 insertions(+), 69 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index b519729345..c10cc1a71b 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include -#include #include "ast/array_decl_plugin.h" #include "util/warning.h" #include "ast/ast_pp.h" @@ -141,8 +140,7 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const * func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* domain) { if (arity != f->get_arity()) { - m_manager->raise_exception(std::format("map expects to take as many arguments as the function being mapped, it was given {} but expects {}", - arity, f->get_arity())); + m_manager->raise_exception("map expects to take as many arguments as the function being mapped, it was given " + std::to_string(arity) + " but expects " + std::to_string(f->get_arity())); return nullptr; } if (arity == 0) { @@ -157,21 +155,21 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* unsigned dom_arity = get_array_arity(domain[0]); for (unsigned i = 0; i < arity; ++i) { if (!is_array_sort(domain[i])) { - m_manager->raise_exception(std::format("map expects an array sort as argument at position {}", i)); + m_manager->raise_exception("map expects an array sort as argument at position " + std::to_string(i)); return nullptr; } if (get_array_arity(domain[i]) != dom_arity) { - m_manager->raise_exception(std::format("map expects all arguments to have the same array domain, this is not the case for argument {}", i)); + m_manager->raise_exception("map expects all arguments to have the same array domain, this is not the case for argument " + std::to_string(i)); return nullptr; } for (unsigned j = 0; j < dom_arity; ++j) { if (get_array_domain(domain[i],j) != get_array_domain(domain[0],j)) { - m_manager->raise_exception(std::format("map expects all arguments to have the same array domain, this is not the case for argument {}", i)); + m_manager->raise_exception("map expects all arguments to have the same array domain, this is not the case for argument " + std::to_string(i)); return nullptr; } } if (get_array_range(domain[i]) != f->get_domain(i)) { - m_manager->raise_exception(std::format("map expects the argument at position {} to have the array range the same as the function", i)); + m_manager->raise_exception("map expects the argument at position " + std::to_string(i) + " to have the array range the same as the function"); return nullptr; } } @@ -232,8 +230,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { parameter const* parameters = s->get_parameters(); if (num_parameters != arity) { - m_manager->raise_exception(std::format("select requires {} arguments, but was provided with {} arguments", - num_parameters, arity)); + m_manager->raise_exception("select requires " + std::to_string(num_parameters) + " arguments, but was provided with " + std::to_string(arity) + " arguments"); return nullptr; } ptr_buffer new_domain; // we need this because of coercions. @@ -242,9 +239,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) { if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast()) || !m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) { - m_manager->raise_exception(std::format("domain sort {} and parameter {} do not match", - to_string(sort_ref(domain[i+1], *m_manager)), - to_string(parameter_pp(parameters[i], *m_manager)))); + m_manager->raise_exception("domain sort " + to_string(sort_ref(domain[i+1], *m_manager)) + " and parameter " + to_string(parameter_pp(parameters[i], *m_manager)) + " do not match"); return nullptr; } new_domain.push_back(to_sort(parameters[i].get_ast())); @@ -268,8 +263,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { return nullptr; } if (arity != num_parameters+1) { - m_manager->raise_exception(std::format("store expects the first argument to be an array taking {}, instead it was passed {} arguments", - num_parameters+1, arity - 1)); + m_manager->raise_exception("store expects the first argument to be an array taking " + std::to_string(num_parameters+1) + ", instead it was passed " + std::to_string(arity - 1) + " arguments"); UNREACHABLE(); return nullptr; } @@ -283,9 +277,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { sort* srt1 = to_sort(parameters[i].get_ast()); sort* srt2 = domain[i+1]; if (!m_manager->compatible_sorts(srt1, srt2)) { - m_manager->raise_exception(std::format("domain sort {} and parameter sort {} do not match", - to_string(sort_ref(srt2, *m_manager)), - to_string(sort_ref(srt1, *m_manager)))); + m_manager->raise_exception("domain sort " + to_string(sort_ref(srt2, *m_manager)) + " and parameter sort " + to_string(sort_ref(srt1, *m_manager)) + " do not match"); UNREACHABLE(); return nullptr; } @@ -318,11 +310,11 @@ func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domai bool array_decl_plugin::check_set_arguments(unsigned arity, sort * const * domain) { for (unsigned i = 0; i < arity; ++i) { if (domain[i] != domain[0]) { - m_manager->raise_exception(std::format("arguments {} and {} have different sorts", 1, i+1)); + m_manager->raise_exception("arguments " + std::to_string(1) + " and " + std::to_string(i+1) + " have different sorts"); return false; } if (domain[i]->get_family_id() != m_family_id) { - m_manager->raise_exception(std::format("argument {} is not of array sort", i+1)); + m_manager->raise_exception("argument " + std::to_string(i+1) + " is not of array sort"); return false; } } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index b0fa217d62..74e5a9f962 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include -#include #include #include "ast/ast.h" #include "ast/ast_pp.h" @@ -1009,9 +1008,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) { return s2; if (s2 == m_bool_sort && s1->get_family_id() == arith_family_id) return s1; - throw ast_exception(std::format("Sorts {} and {} are incompatible", - to_string(mk_pp(s1, *m_manager)), - to_string(mk_pp(s2, *m_manager)))); + throw ast_exception("Sorts " + to_string(mk_pp(s1, *m_manager)) + " and " + to_string(mk_pp(s2, *m_manager)) + " are incompatible"); } @@ -1675,8 +1672,7 @@ ast * ast_manager::register_node_core(ast * n) { SASSERT(contains); SASSERT(m_ast_table.contains(n)); if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) { - throw ast_exception(std::format("Recycling of declaration for the same name '{}' and domain, but different range type is not permitted", - to_func_decl(r)->get_name().str())); + throw ast_exception(std::string("Recycling of declaration for the same name '") + to_func_decl(r)->get_name().str() + "' and domain, but different range type is not permitted"); } deallocate_node(n, ::get_node_size(n)); return r; @@ -1994,11 +1990,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c for (unsigned i = 0; i < num_args; ++i) { sort * given = args[i]->get_sort(); if (!compatible_sorts(expected, given)) { - throw ast_exception(std::format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}", - to_string(decl->get_name()), - i + 1, - to_string(mk_pp(expected, m)), - to_string(mk_pp(given, m)))); + throw ast_exception("invalid function application for " + to_string(decl->get_name()) + ", sort mismatch on argument at position " + std::to_string(i + 1) + ", expected " + to_string(mk_pp(expected, m)) + " but given " + to_string(mk_pp(given, m))); } } } @@ -2010,11 +2002,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c sort * expected = decl->get_domain(i); sort * given = args[i]->get_sort(); if (!compatible_sorts(expected, given)) { - throw ast_exception(std::format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}", - to_string(decl->get_name()), - i + 1, - to_string(mk_pp(expected, m)), - to_string(mk_pp(given, m)))); + throw ast_exception("invalid function application for " + to_string(decl->get_name()) + ", sort mismatch on argument at position " + std::to_string(i + 1) + ", expected " + to_string(mk_pp(expected, m)) + " but given " + to_string(mk_pp(given, m))); } } } @@ -2169,10 +2157,7 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) { sort * actual_sort = es[i]->get_sort(); sort * expected_sort = f->is_associative() ? f->get_domain(0) : f->get_domain(i); if (expected_sort != actual_sort) { - throw ast_exception(std::format("Sort mismatch at argument #{} for function {} supplied sort is {}", - i + 1, - to_string(mk_pp(f, *this)), - to_string(mk_pp(actual_sort, *this)))); + throw ast_exception("Sort mismatch at argument #" + std::to_string(i + 1) + " for function " + to_string(mk_pp(f, *this)) + " supplied sort is " + to_string(mk_pp(actual_sort, *this))); } } } @@ -2195,11 +2180,8 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar if (type_error) { std::string arg_list; for (unsigned i = 0; i < num_args; ++i) - arg_list += std::format("\narg: {}\n", to_string(mk_pp(args[i], *this))); - throw ast_exception(std::format("Wrong number of arguments ({}) passed to function {} {}", - num_args, - to_string(mk_pp(decl, *this)), - arg_list)); + arg_list += "\narg: " + to_string(mk_pp(args[i], *this)) + "\n"; + throw ast_exception("Wrong number of arguments (" + std::to_string(num_args) + ") passed to function " + to_string(mk_pp(decl, *this)) + " " + arg_list); } app * r = nullptr; if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) { diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index bb65581cce..0ae6097341 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include -#include #include "ast/bv_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "util/warning.h" @@ -673,11 +672,7 @@ 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)) { - 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)))); + m.raise_exception("Argument " + to_string(mk_pp(args[i], m)) + " at position " + std::to_string(i) + " has sort " + to_string(mk_pp(args[i]->get_sort(), m)) + " it does not match declaration " + 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 d875262b38..7c75659cff 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include -#include #include "util/warning.h" #include "ast/array_decl_plugin.h" #include "ast/seq_decl_plugin.h" @@ -379,9 +378,7 @@ namespace datatype { return nullptr; } if (rng != domain[1]) { - 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)))); + m.raise_exception("second argument to field update should be " + to_string(mk_ismt2_pp(rng, m)) + " instead of " + 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 1be709324c..f0c271af93 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -17,7 +17,6 @@ Revision History: --*/ #include -#include #include "ast/ast_pp.h" #include "ast/array_decl_plugin.h" @@ -53,7 +52,7 @@ namespace datalog { if (low <= val && val <= up) { return true; } - m_manager->raise_exception(std::format("{}, value is not within bound {} <= {} <= {}", msg, low, val, up)); + m_manager->raise_exception(std::string(msg) + ", value is not within bound " + std::to_string(low) + " <= " + std::to_string(val) + " <= " + std::to_string(up)); return false; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 75949316a0..1bdb91cb48 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -21,7 +21,7 @@ Revision History: #include "ast/array_decl_plugin.h" #include "ast/ast_pp.h" #include -#include + seq_decl_plugin::seq_decl_plugin(): m_init(false), @@ -83,8 +83,7 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor ptr_vector binding; ast_manager& m = *m_manager; if (dsz == 0) { - m.raise_exception(std::format("Unexpected number of arguments to '{}' at least one argument expected {} given", - sig.m_name.str(), dsz)); + m.raise_exception("Unexpected number of arguments to '" + std::string(sig.m_name.str()) + "' at least one argument expected " + std::to_string(dsz) + " given"); } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { @@ -101,10 +100,9 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor } std::string range_str; if (range) { - range_str = std::format(" and range: {}", to_string(mk_pp(range, m))); + range_str = " and range: " + to_string(mk_pp(range, m)); } - m.raise_exception(std::format("Sort of function '{}' does not match the declared type. Given domain: {}{}", - sig.m_name.str(), domain_str, range_str)); + m.raise_exception("Sort of function '" + std::string(sig.m_name.str()) + "' does not match the declared type. Given domain: " + domain_str + range_str); } range_out = apply_binding(binding, sig.m_range); SASSERT(range_out); @@ -114,8 +112,7 @@ 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) { - m.raise_exception(std::format("Unexpected number of arguments to '{}' {} arguments expected {} given", - sig.m_name.str(), sig.m_dom.size(), dsz)); + m.raise_exception("Unexpected number of arguments to '" + std::string(sig.m_name.str()) + "' " + std::to_string(sig.m_dom.size()) + " arguments expected " + std::to_string(dsz) + " given"); } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { @@ -131,19 +128,17 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran } std::string range_str; if (range) { - range_str = std::format(" and range: {}", to_string(mk_pp(range, m))); + range_str = " and range: " + to_string(mk_pp(range, m)); } std::string expected_domain; for (unsigned i = 0; i < dsz; ++i) { expected_domain += to_string(mk_pp(sig.m_dom[i].get(), m)) + " "; } - 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)); + m.raise_exception("Sort of polymorphic function '" + std::string(sig.m_name.str()) + "' does not match the declared type. \nGiven domain: " + given_domain + range_str + "\nExpected domain: " + expected_domain); } if (!range && dsz == 0) { - 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())); + m.raise_exception("Sort of polymorphic function '" + std::string(sig.m_name.str()) + "' is ambiguous. Function takes no arguments and sort of range has not been constrained"); } range_out = apply_binding(m_binding, sig.m_range); SASSERT(range_out);