mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix #7523

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-22 11:45:02 -08:00
parent 4fce314bf2
commit ef275ab1a0
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_numeral.cpp
View file

@ -235,9 +235,7 @@ extern "C" {
}
}
else if (mk_c(c)->fpautil().is_numeral(to_expr(a), tmp)) {
std::ostringstream buffer;
fu.fm().display_smt2(buffer, tmp, false);
return mk_c(c)->mk_external_string(std::move(buffer).str());
return mk_c(c)->mk_external_string(fu.fm().to_rational_string(tmp));
}
else {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);