mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

x64 clause allocator fix for del_clause

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-08-23 18:46:14 +01:00
parent 5b1cb49973
commit b70cc47a9d
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/sat_clause.cpp
View file

@ -207,6 +207,11 @@ namespace sat {
void clause_allocator::del_clause(clause * cls) {
TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
m_id_gen.recycle(cls->id());
#if defined(_AMD64_)
#if defined(Z3DEBUG)
m_last_seg_id2cls.remove(cls->id());
#endif
#endif
size_t size = clause::get_obj_size(cls->m_capacity);
cls->~clause();
m_allocator.deallocate(size, cls);