mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

Apply patch submitted by David Cok

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-06-05 14:11:11 -07:00
parent 095ba806ab
commit 38d1f30dba
1 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/watch_list.cpp
View file

@ -48,12 +48,17 @@ namespace smt {
*mem = DEFAULT_WATCH_LIST_SIZE; *mem = DEFAULT_WATCH_LIST_SIZE;
++mem; ++mem;
m_data = reinterpret_cast<char*>(mem); m_data = reinterpret_cast<char*>(mem);
SASSERT( begin_lits_core() % sizeof(literal) == 0 );
} }
else { else {
unsigned curr_begin_bin = begin_lits_core(); unsigned curr_begin_bin = begin_lits_core();
unsigned curr_capacity = end_lits_core(); unsigned curr_capacity = end_lits_core();
unsigned bin_bytes = curr_capacity - curr_begin_bin; unsigned bin_bytes = curr_capacity - curr_begin_bin;
unsigned new_capacity = (curr_capacity * 3 + sizeof(clause *)) >> 1; /* dvitek: Added +3&~3U to fix alignment issues on
* sparc64/solaris. ("literal"s must be 4-byte aligned). Should
* also help performance elsewhere.
*/
unsigned new_capacity = (((curr_capacity * 3 + sizeof(clause *)) >> 1)+3)&~3U;
unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, new_capacity + HEADER_SIZE)); unsigned * mem = reinterpret_cast<unsigned*>(alloc_svect(char, new_capacity + HEADER_SIZE));
unsigned curr_end_cls = end_cls_core(); unsigned curr_end_cls = end_cls_core();
#ifdef _AMD64_ #ifdef _AMD64_
@ -71,6 +76,7 @@ namespace smt {
memcpy(reinterpret_cast<char *>(mem) + new_begin_bin, m_data + curr_begin_bin, bin_bytes); memcpy(reinterpret_cast<char *>(mem) + new_begin_bin, m_data + curr_begin_bin, bin_bytes);
destroy(); destroy();
m_data = reinterpret_cast<char *>(mem); m_data = reinterpret_cast<char *>(mem);
SASSERT( begin_lits_core() % sizeof(literal) == 0 );
} }
} }