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 bugs reported by Nuno Lopes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-06-04 12:55:35 -07:00
parent aa0d921240
commit b6d9d8a601
3 changed files with 11 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/qe_lite.cpp
View file

@ -1417,6 +1417,7 @@ namespace fm {
fm(ast_manager & _m): fm(ast_manager & _m):
m(_m), m(_m),
m_is_variable(0),
m_allocator("fm-elim"), m_allocator("fm-elim"),
m_util(m), m_util(m),
m_bvar2expr(m), m_bvar2expr(m),
@ -1424,6 +1425,9 @@ namespace fm {
m_new_fmls(m), m_new_fmls(m),
m_inconsistent_core(m) { m_inconsistent_core(m) {
m_cancel = false; m_cancel = false;
updt_params();
m_counter = 0;
m_inconsistent = false;
} }
~fm() { ~fm() {

10
src/util/bit_vector.cpp
View file

@ -22,6 +22,8 @@ Revision History:
#define DEFAULT_CAPACITY 2 #define DEFAULT_CAPACITY 2
#define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1)
void bit_vector::expand_to(unsigned new_capacity) { void bit_vector::expand_to(unsigned new_capacity) {
unsigned * new_data = alloc_svect(unsigned, new_capacity); unsigned * new_data = alloc_svect(unsigned, new_capacity);
memset(new_data, 0, new_capacity * sizeof(unsigned)); memset(new_data, 0, new_capacity * sizeof(unsigned));
@ -51,7 +53,7 @@ void bit_vector::resize(unsigned new_size, bool val) {
unsigned ewidx = num_words(new_size); unsigned ewidx = num_words(new_size);
unsigned * begin = m_data + bwidx; unsigned * begin = m_data + bwidx;
unsigned pos = m_num_bits % 32; unsigned pos = m_num_bits % 32;
unsigned mask = (1 << pos) - 1; unsigned mask = MK_MASK(pos);
int cval; int cval;
if (val) { if (val) {
@ -128,7 +130,7 @@ bool bit_vector::operator==(bit_vector const & source) const {
return false; return false;
} }
unsigned bit_rest = source.m_num_bits % 32; unsigned bit_rest = source.m_num_bits % 32;
unsigned mask = (1 << bit_rest) - 1; unsigned mask = MK_MASK(bit_rest);
if (mask == 0) mask = UINT_MAX; if (mask == 0) mask = UINT_MAX;
return (m_data[i] & mask) == (source.m_data[i] & mask); return (m_data[i] & mask) == (source.m_data[i] & mask);
} }
@ -149,7 +151,7 @@ bit_vector & bit_vector::operator|=(bit_vector const & source) {
unsigned i = 0; unsigned i = 0;
for (i = 0; i < n2 - 1; i++) for (i = 0; i < n2 - 1; i++)
m_data[i] |= source.m_data[i]; m_data[i] |= source.m_data[i];
unsigned mask = (1 << bit_rest) - 1; unsigned mask = MK_MASK(bit_rest);
m_data[i] |= source.m_data[i] & mask; m_data[i] |= source.m_data[i] & mask;
} }
return *this; return *this;
@ -175,7 +177,7 @@ bit_vector & bit_vector::operator&=(bit_vector const & source) {
else { else {
for (i = 0; i < n2 - 1; i++) for (i = 0; i < n2 - 1; i++)
m_data[i] &= source.m_data[i]; m_data[i] &= source.m_data[i];
unsigned mask = (1 << bit_rest) - 1; unsigned mask = MK_MASK(bit_rest);
m_data[i] &= (source.m_data[i] & mask); m_data[i] &= (source.m_data[i] & mask);
} }

1
src/util/bit_vector.h
View file

@ -69,6 +69,7 @@ public:
m_num_bits(0), m_num_bits(0),
m_capacity(num_words(reserve_num_bits)), m_capacity(num_words(reserve_num_bits)),
m_data(alloc_svect(unsigned, m_capacity)) { m_data(alloc_svect(unsigned, m_capacity)) {
memset(m_data, 0, m_capacity * sizeof(unsigned));
} }
bit_vector(bit_vector const & source): bit_vector(bit_vector const & source):