mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 11:35:42 +00:00
Code Activity

Fix Mac Build x64 CI failure: replace std::format with string concatenation

Browse source 
std::format requires MACOSX_DEPLOYMENT_TARGET >= 13.3 because libc++'s
<format> 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 <format>
from each file.
This commit is contained in:
copilot-swe-agent[bot] 2026-07-10 22:10:41 +00:00 • committed by GitHub
parent 46968d4628
commit 241d77185a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 29 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/seq_decl_plugin.cpp
View file

@ -21,7 +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),
@ -83,8 +83,7 @@ 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) {
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);