From 43465accc62b456ab4d548b9dbdf7bcdf09c3893 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 18 Nov 2025 10:28:25 -1000 Subject: [PATCH] add coefficients from the elim_vanishing to m_todo Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 8cefd9fa8..efe55ae39 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -350,20 +350,12 @@ namespace nlsat { } lc = m_pm.coeff(p, x, k, reduct); TRACE(nlsat_explain, tout << "lc: " << lc << " reduct: " << reduct << "\n";); - if (!is_zero(lc)) { - if (!::is_zero(sign(lc))) { - TRACE(nlsat_explain, tout << "lc does no vaninsh\n";); - return; - } - TRACE(nlsat_explain, tout << "got a zero sign on lc\n";); - - - // lc is not the zero polynomial, but it vanished in the current interpretation. - // so we keep searching... - TRACE(nlsat_explain, tout << "adding zero assumption for var:"; m_solver.display_var(tout, x); tout << ", degree k:" << k << ", p:" ; display(tout, p) << "\n";); - - add_zero_assumption(lc); + insert_fresh_factors_in_todo(lc); + if (!is_zero(lc) && sign(lc)) { + TRACE(nlsat_explain, tout << "lc does no vaninsh\n";); + return; } + add_zero_assumption(lc); if (k == 0) { // all coefficients of p vanished in the current interpretation, // and were added as assumptions.