mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Fix bug in compare

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-12 16:44:39 -08:00
parent ea9421bb38
commit a9fa232f11
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/math/realclosure/realclosure.cpp
View file

@ -881,10 +881,7 @@ namespace realclosure {
\brief Return true if v is the value one; \brief Return true if v is the value one;
*/ */
bool is_one(value * v) const { bool is_one(value * v) const {
if (is_rational_one(v)) return const_cast<imp*>(this)->compare(v, one()) == 0;
return true;
// TODO: check if v is equal to one.
return false;
} }
/** /**
@ -4743,8 +4740,12 @@ namespace realclosure {
return -sign(b); return -sign(b);
else if (b == 0) else if (b == 0)
return sign(a); return sign(a);
else if (is_nz_rational(a) && is_nz_rational(b)) else if (is_nz_rational(a) && is_nz_rational(b)) {
return qm().lt(to_mpq(a), to_mpq(b)) ? -1 : 1; if (qm().eq(to_mpq(a), to_mpq(b)))
return 0;
else
return qm().lt(to_mpq(a), to_mpq(b)) ? -1 : 1;
}
else { else {
// FUTURE: try to refine interval before switching to sub+sign approach // FUTURE: try to refine interval before switching to sub+sign approach
if (bqim().before(interval(a), interval(b))) if (bqim().before(interval(a), interval(b)))