mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 03:31:23 +00:00
Code Activity

fix bug reported in #1637

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-22 20:02:08 -07:00
parent ad973d5c6d
commit 363d7aad2a
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/nlsat/nlsat_explain.cpp
View file

@ -1463,6 +1463,7 @@ namespace nlsat {
void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) { void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) {
m_result = &result; m_result = &result;
svector<literal> lits; svector<literal> lits;
TRACE("nlsat", tout << "project x" << x << "\n"; m_solver.display(tout);); TRACE("nlsat", tout << "project x" << x << "\n"; m_solver.display(tout););
@ -1643,6 +1644,7 @@ namespace nlsat {
++num_lub; ++num_lub;
} }
} }
TRACE("nlsat_explain", tout << ps << "\n";);
if (num_lub == 0) { if (num_lub == 0) {
project_plus_infinity(x, ps); project_plus_infinity(x, ps);
@ -1668,7 +1670,7 @@ namespace nlsat {
unsigned d = degree(p, x); unsigned d = degree(p, x);
lc = m_pm.coeff(p, x, d); lc = m_pm.coeff(p, x, d);
if (!is_const(lc)) { if (!is_const(lc)) {
unsigned s = sign(p); int s = sign(p);
SASSERT(s != 0); SASSERT(s != 0);
atom::kind k = (s > 0)?(atom::GT):(atom::LT); atom::kind k = (s > 0)?(atom::GT):(atom::LT);
add_simple_assumption(k, lc); add_simple_assumption(k, lc);
@ -1683,7 +1685,8 @@ namespace nlsat {
unsigned d = degree(p, x); unsigned d = degree(p, x);
lc = m_pm.coeff(p, x, d); lc = m_pm.coeff(p, x, d);
if (!is_const(lc)) { if (!is_const(lc)) {
unsigned s = sign(p); int s = sign(p);
TRACE("nlsat_explain", tout << "degree: " << d << " " << lc << " sign: " << s << "\n";);
SASSERT(s != 0); SASSERT(s != 0);
atom::kind k; atom::kind k;
if (s > 0) { if (s > 0) {