mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
again
This commit is contained in:
parent
bb6c274ad3
commit
cc045debac
|
@ -2248,7 +2248,10 @@ template<bool SYNCH>
|
|||
unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
|
||||
if (is_nonneg(a))
|
||||
return 0;
|
||||
if (is_small(a) && a.m_val > INT_MIN)
|
||||
if (is_small(a) && a.m_val == INT_MIN)
|
||||
return ::log2((unsigned)a.m_val);
|
||||
|
||||
if (is_small(a))
|
||||
return ::log2((unsigned)-a.m_val);
|
||||
#ifndef _MP_GMP
|
||||
static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, "");
|
||||
|
|
Loading…
Reference in a new issue