From cb83dedbd2a2bff754969760c6ff410c9205a890 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 13 Nov 2025 18:40:43 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_solver.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index c28e3aada..f7ff54223 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -3357,9 +3357,14 @@ namespace nlsat { out << "(assert (= "; proc(out, x); out << " "; - mpq q; - m_am.to_rational(m_assignment.value(x), q); - m_am.qm().display_smt2(out, q, false); + if (m_am.is_rational(m_assignment.value(x))) { + mpq q; + m_am.to_rational(m_assignment.value(x), q); + m_am.qm().display_smt2(out, q, false); + } + else { + m_am.display_root_smt2(out, m_assignment.value(x)); + } out << "))\n"; } else {