mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #3559

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-30 14:00:30 -07:00
parent de2ad26826
commit e263f9b238
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/util/mpz.cpp
View file

@ -1780,10 +1780,10 @@ void mpz_manager<SYNCH>::display_hex(std::ostream & out, mpz const & a, unsigned
out.copyfmt(fmt);
}
void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) {
for (unsigned shift = numBits; shift-- > 32; ) out << "0";
for (unsigned shift = std::min(32u, numBits); shift-- > 0; ) {
if (val & (1 << shift)) {
static void display_binary_data(std::ostream &out, uint64_t val, uint64_t numBits) {
for (uint64_t shift = numBits; shift-- > 64ull; ) out << "0";
for (uint64_t shift = std::min(64ull, numBits); shift-- > 0; ) {
if (val & (1ull << shift)) {
out << "1";
} else {
out << "0";
@ -1793,9 +1793,9 @@ void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) {
template<bool SYNCH>
void mpz_manager<SYNCH>::display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const {
if (is_uint(a)) {
display_binary_data(out, get_uint(a), num_bits);
}
if (is_small(a)) {
display_binary_data(out, get_uint64(a), num_bits);
}
else {
#ifndef _MP_GMP
digit_t *ds = digits(a);