mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

Fix bug in sprem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-12 19:44:05 -08:00
parent 7711146d23
commit 551d0b7de0
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2931,7 +2931,7 @@ namespace realclosure {
unsigned d; unsigned d;
prem(sz1, p1, sz2, p2, d, r); prem(sz1, p1, sz2, p2, d, r);
// We should not flip the sign if d is odd and leading coefficient of p2 is negative. // We should not flip the sign if d is odd and leading coefficient of p2 is negative.
if (d % 2 == 0 || (sz2 > 0 && sign(p2[sz2-1]) < 0)) if (d % 2 == 0 || (sz2 > 0 && sign(p2[sz2-1]) > 0))
neg(r); neg(r);
} }