From ef275ab1a01693a03a581e90aad4a1d289c6ef5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Jan 2025 11:45:02 -0800 Subject: [PATCH] fix #7523 --- src/api/api_numeral.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 4e99e05f01..614395240b 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -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);