mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #3392

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-18 09:47:23 -07:00
parent 752b498254
commit a45532da73
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/nlsat_solver.cpp
View file

@ -2676,6 +2676,7 @@ namespace nlsat {
scoped_anum pv(m_am), qv(m_am), val(m_am); scoped_anum pv(m_am), qv(m_am), val(m_am);
m_pm.eval(p, m_assignment, pv); m_pm.eval(p, m_assignment, pv);
m_pm.eval(q, m_assignment, qv); m_pm.eval(q, m_assignment, qv);
SASSERT(!m_am.is_zero(pv));
val = qv / pv; val = qv / pv;
TRACE("nlsat", TRACE("nlsat",
m_display_var(tout << "patch v" << v << " ", v) << "\n"; m_display_var(tout << "patch v" << v << " ", v) << "\n";
@ -2879,6 +2880,8 @@ namespace nlsat {
if (m_is_int[x]) continue; if (m_is_int[x]) continue;
if (1 == m_pm.degree(p0, x)) { if (1 == m_pm.degree(p0, x)) {
p = m_pm.coeff(p0, x, 1, q); p = m_pm.coeff(p0, x, 1, q);
if (!m_pm.is_const(p))
break;
switch (m_pm.sign(p, m_var_signs)) { switch (m_pm.sign(p, m_var_signs)) {
case l_true: case l_true:
v = x; v = x;