mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-31 19:29:13 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-12 10:24:31 +01:00
commit a6bb7d2d0f
3 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/bit_util.cpp
View file

@ -351,7 +351,7 @@ bool has_one_at_first_k_bits(unsigned sz, unsigned const * data, unsigned k) {
} }
if (word_sz < sz) { if (word_sz < sz) {
unsigned bit_sz = k % (8 * sizeof(unsigned)); unsigned bit_sz = k % (8 * sizeof(unsigned));
unsigned mask = (1 << bit_sz) - 1; unsigned mask = (1u << bit_sz) - 1;
return (data[word_sz] & mask) != 0; return (data[word_sz] & mask) != 0;
} }
return false; return false;

10
src/util/bit_vector.h
View file

@ -75,8 +75,11 @@ public:
bit_vector(bit_vector const & source): bit_vector(bit_vector const & source):
m_num_bits(source.m_num_bits), m_num_bits(source.m_num_bits),
m_capacity(source.m_capacity), m_capacity(source.m_capacity),
m_data(alloc_svect(unsigned, source.m_capacity)) { m_data(0) {
memcpy(m_data, source.m_data, source.m_capacity * sizeof(unsigned)); if (source.m_data) {
m_data = alloc_svect(unsigned, m_capacity);
memcpy(m_data, source.m_data, m_capacity * sizeof(unsigned));
}
} }
bit_vector(unsigned const * source, int num_bits): bit_vector(unsigned const * source, int num_bits):
@ -184,6 +187,9 @@ public:
bit_vector & operator=(bit_vector const & source) { bit_vector & operator=(bit_vector const & source) {
m_num_bits = source.m_num_bits; m_num_bits = source.m_num_bits;
if (!source.m_data)
return *this;
if (m_capacity < source.m_capacity) { if (m_capacity < source.m_capacity) {
dealloc_svect(m_data); dealloc_svect(m_data);
m_data = alloc_svect(unsigned, source.m_capacity); m_data = alloc_svect(unsigned, source.m_capacity);

4
src/util/mpff.cpp
View file

@ -255,7 +255,7 @@ void mpff_manager::set(mpff & n, int64 v) {
} }
else { else {
if (v < 0) { if (v < 0) {
set(n, static_cast<uint64>(-v)); set(n, -static_cast<uint64>(v));
n.m_sign = 1; n.m_sign = 1;
} }
else { else {
@ -680,7 +680,7 @@ void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c
// Make sure that a and b have the same exponent. // Make sure that a and b have the same exponent.
if (exp_a > exp_b) { if (exp_a > exp_b) {
unsigned shift = exp_a - exp_b; unsigned shift = (unsigned)exp_a - (unsigned)exp_b;
n_sig_b = m_buffers[0].c_ptr(); n_sig_b = m_buffers[0].c_ptr();
shr(m_precision, sig_b, shift, m_precision, n_sig_b); shr(m_precision, sig_b, shift, m_precision, n_sig_b);
if (sgn_b != m_to_plus_inf && has_one_at_first_k_bits(m_precision, sig_b, shift)) { if (sgn_b != m_to_plus_inf && has_one_at_first_k_bits(m_precision, sig_b, shift)) {