fix #7523

Z3Prover · Jan 22, 2025 · ef275ab · ef275ab
1 parent 4fce314
commit ef275ab
Showing 1 changed file with 1 addition and 3 deletions.
diff --git 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);