3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-19 16:41:28 -07:00
parent a1d3acab29
commit f8df7770a2

View file

@ -1354,9 +1354,9 @@ namespace nlsat {
var max = max_var(num, ls);
SASSERT(max != null_var);
normalize(m_core2, max);
TRACE("nlsat_explain", tout << "core after normalization\n"; display(tout, m_core2););
TRACE("nlsat_explain", tout << "core after normalization\n"; display(tout, m_core2) << "\n";);
simplify(m_core2, max);
TRACE("nlsat_explain", tout << "core after simplify\n"; display(tout, m_core2););
TRACE("nlsat_explain", tout << "core after simplify\n"; display(tout, m_core2) << "\n";);
main(m_core2.size(), m_core2.c_ptr());
m_core2.reset();
}
@ -1454,7 +1454,7 @@ namespace nlsat {
process(num, ls);
reset_already_added();
m_result = nullptr;
TRACE("nlsat_explain", display(tout << "[explain] result\n", result););
TRACE("nlsat_explain", display(tout << "[explain] result\n", result) << "\n";);
CASSERT("nlsat", check_already_added());
}