mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-02 07:16:17 +00:00
Code Activity

cosmetics

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-05 06:13:37 -10:00
parent 0ccf23428d
commit 5985f9bd34
2 changed files with 0 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_explain.cpp
View file

@ -1129,7 +1129,6 @@ namespace nlsat {
bool first = true;
if (ps.empty())
return;
TRACE(nlsat_explain, ::nlsat::display(tout << "ps:", m_solver, ps)<< "\n";);
m_todo.reset();
for (unsigned i = 0; i < ps.size(); i++) {
polynomial_ref p(m_pm);
@ -1147,10 +1146,7 @@ namespace nlsat {
if (levelwise_ok)
return;
}
TRACE(nlsat_explain, ::nlsat::display(tout << "ps before extract:", m_solver, ps)<< "\n";);
var x = m_todo.extract_max_polys(ps);
TRACE(nlsat_explain, ::nlsat::display(tout << "ps:", m_solver, ps)<< "\n";);
polynomial_ref_vector samples(m_pm);
if (x < max_x)
cac_add_cell_lits(ps, x, samples);