mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 05:36:41 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-13 18:40:43 -10:00
parent b8efb77c0c
commit cb83dedbd2
1 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/nlsat/nlsat_solver.cpp
View file

@ -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 {