From 38d1f30dba0661792c3f208a3542b0d835b92405 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jun 2013 14:11:11 -0700 Subject: [PATCH] Apply patch submitted by David Cok Signed-off-by: Leonardo de Moura --- src/smt/watch_list.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp index 731e021fe..ed73b9ed5 100644 --- a/src/smt/watch_list.cpp +++ b/src/smt/watch_list.cpp @@ -48,12 +48,17 @@ namespace smt { *mem = DEFAULT_WATCH_LIST_SIZE; ++mem; m_data = reinterpret_cast(mem); + SASSERT( begin_lits_core() % sizeof(literal) == 0 ); } else { unsigned curr_begin_bin = begin_lits_core(); unsigned curr_capacity = end_lits_core(); 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(alloc_svect(char, new_capacity + HEADER_SIZE)); unsigned curr_end_cls = end_cls_core(); #ifdef _AMD64_ @@ -71,6 +76,7 @@ namespace smt { memcpy(reinterpret_cast(mem) + new_begin_bin, m_data + curr_begin_bin, bin_bytes); destroy(); m_data = reinterpret_cast(mem); + SASSERT( begin_lits_core() % sizeof(literal) == 0 ); } }