From 3499fa7f0bf968961e81246ee46e9f34973089ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Mar 2020 05:01:44 -0800 Subject: [PATCH] fix #3106 Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 3 ++- src/nlsat/tactic/goal2nlsat.cpp | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) 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()); }