diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 419963e58..dad39527d 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -587,8 +587,9 @@ namespace nlsat { var max = null_var; for (unsigned i = 0; i < sz; i++) { p = m_pm.flip_sign_if_lm_neg(ps[i]); - if (p.get() != ps[i]) + if (p.get() != ps[i] && !is_even[i]) { sign = -sign; + } var curr_max = max_var(p.get()); if (curr_max > max || max == null_var) max = curr_max; diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp index 4c4483d1f..599f248e8 100644 --- a/src/nlsat/tactic/goal2nlsat.cpp +++ b/src/nlsat/tactic/goal2nlsat.cpp @@ -104,8 +104,8 @@ struct goal2nlsat::imp { ps.push_back(fs[i]); is_even.push_back(fs.get_degree(i) % 2 == 0); } - if (m_qm.is_neg(fs.get_constant())) - k = flip(k); + if (m_qm.is_neg(fs.get_constant())) + k = flip(k); return m_solver.mk_ineq_atom(k, ps.size(), ps.c_ptr(), is_even.c_ptr()); }