mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

restore the method behavior

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-15 16:41:32 -07:00 • committed by Nikolaj Bjorner
parent d9ca739499
commit 351c0401fb
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/nlsat/nlsat_explain.cpp
View file

@ -1245,8 +1245,6 @@ namespace nlsat {
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
polynomial_ref_vector samples(m_pm); polynomial_ref_vector samples(m_pm);
if (x < max_x) if (x < max_x)
cac_add_cell_lits(ps, x, samples); cac_add_cell_lits(ps, x, samples);
@ -1257,7 +1255,8 @@ namespace nlsat {
} }
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
display(tout, ps); tout << "\n";); display(tout, ps); tout << "\n";);
if (first) { if (first) { // The first run is special because x is not constrained by the sample, we cannot surround it by the root functions.
// we make the polynomials in ps delinable
add_lcs(ps, x); add_lcs(ps, x);
psc_discriminant(ps, x); psc_discriminant(ps, x);
psc_resultant(ps, x); psc_resultant(ps, x);